Theorem writeisf ≪ | index | src | ≫ 

theorem writeisf (F: set) (a b: nat): $ isfun F -> isfun (write F a b) $;
StepHypRefExpression
1 elwrite 
x, y e. write F a b <-> ifp (x = a) (y = b) (x, y e. F)
2 elwrite 
x, z e. write F a b <-> ifp (x = a) (z = b) (x, z e. F)
3 ifppos 
x = a -> (ifp (x = a) (z = b) (x, z e. F) <-> z = b)
4 anrl 
isfun F /\ (x = a /\ y = b) -> x = a
5 3, 4 syl 
isfun F /\ (x = a /\ y = b) -> (ifp (x = a) (z = b) (x, z e. F) <-> z = b)
6 5 imeq1d 
isfun F /\ (x = a /\ y = b) -> (ifp (x = a) (z = b) (x, z e. F) -> y = z <-> z = b -> y = z)
7 eqtr4 
y = b -> z = b -> y = z
8 anrr 
isfun F /\ (x = a /\ y = b) -> y = b
9 7, 8 syl 
isfun F /\ (x = a /\ y = b) -> z = b -> y = z
10 6, 9 mpbird 
isfun F /\ (x = a /\ y = b) -> ifp (x = a) (z = b) (x, z e. F) -> y = z
11 2, 10 syl5bi 
isfun F /\ (x = a /\ y = b) -> x, z e. write F a b -> y = z
12 ifpneg 
~x = a -> (ifp (x = a) (z = b) (x, z e. F) <-> x, z e. F)
13 anrl 
isfun F /\ (~x = a /\ x, y e. F) -> ~x = a
14 12, 13 syl 
isfun F /\ (~x = a /\ x, y e. F) -> (ifp (x = a) (z = b) (x, z e. F) <-> x, z e. F)
15 14 imeq1d 
isfun F /\ (~x = a /\ x, y e. F) -> (ifp (x = a) (z = b) (x, z e. F) -> y = z <-> x, z e. F -> y = z)
16 anll 
isfun F /\ (~x = a /\ x, y e. F) /\ x, z e. F -> isfun F
17 anrr 
isfun F /\ (~x = a /\ x, y e. F) -> x, y e. F
18 17 anwl 
isfun F /\ (~x = a /\ x, y e. F) /\ x, z e. F -> x, y e. F
19 anr 
isfun F /\ (~x = a /\ x, y e. F) /\ x, z e. F -> x, z e. F
20 16, 18, 19 isfd 
isfun F /\ (~x = a /\ x, y e. F) /\ x, z e. F -> y = z
21 20 exp 
isfun F /\ (~x = a /\ x, y e. F) -> x, z e. F -> y = z
22 15, 21 mpbird 
isfun F /\ (~x = a /\ x, y e. F) -> ifp (x = a) (z = b) (x, z e. F) -> y = z
23 2, 22 syl5bi 
isfun F /\ (~x = a /\ x, y e. F) -> x, z e. write F a b -> y = z
24 11, 23 eorda 
isfun F -> x = a /\ y = b \/ ~x = a /\ x, y e. F -> x, z e. write F a b -> y = z
25 24 conv ifp 
isfun F -> ifp (x = a) (y = b) (x, y e. F) -> x, z e. write F a b -> y = z
26 1, 25 syl5bi 
isfun F -> x, y e. write F a b -> x, z e. write F a b -> y = z
27 26 iald 
isfun F -> A. z (x, y e. write F a b -> x, z e. write F a b -> y = z)
28 27 iald 
isfun F -> A. y A. z (x, y e. write F a b -> x, z e. write F a b -> y = z)
29 28 iald 
isfun F -> A. x A. y A. z (x, y e. write F a b -> x, z e. write F a b -> y = z)
30 29 conv isfun 
isfun F -> isfun (write F a b)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)