Theorem isfd ≪ | index | src | ≫ 

theorem isfd (F: set) (G: wff) (a b b2: nat):
  $ G -> isfun F $ >
  $ G -> a, b e. F $ >
  $ G -> a, b2 e. F $ >
  $ G -> b = b2 $;
StepHypRefExpression
1 hyp h3 
G -> a, b2 e. F
2 hyp h2 
G -> a, b e. F
3 hyp h1 
G -> isfun F
4 anllr 
G /\ x = a /\ y = b /\ z = b2 -> x = a
5 anlr 
G /\ x = a /\ y = b /\ z = b2 -> y = b
6 4, 5 preqd 
G /\ x = a /\ y = b /\ z = b2 -> x, y = a, b
7 6 eleq1d 
G /\ x = a /\ y = b /\ z = b2 -> (x, y e. F <-> a, b e. F)
8 anr 
G /\ x = a /\ y = b /\ z = b2 -> z = b2
9 4, 8 preqd 
G /\ x = a /\ y = b /\ z = b2 -> x, z = a, b2
10 9 eleq1d 
G /\ x = a /\ y = b /\ z = b2 -> (x, z e. F <-> a, b2 e. F)
11 5, 8 eqeqd 
G /\ x = a /\ y = b /\ z = b2 -> (y = z <-> b = b2)
12 10, 11 imeqd 
G /\ x = a /\ y = b /\ z = b2 -> (x, z e. F -> y = z <-> a, b2 e. F -> b = b2)
13 7, 12 imeqd 
G /\ x = a /\ y = b /\ z = b2 -> (x, y e. F -> x, z e. F -> y = z <-> a, b e. F -> a, b2 e. F -> b = b2)
14 13 bi1d 
G /\ x = a /\ y = b /\ z = b2 -> (x, y e. F -> x, z e. F -> y = z) -> a, b e. F -> a, b2 e. F -> b = b2
15 14 ealde 
G /\ x = a /\ y = b -> A. z (x, y e. F -> x, z e. F -> y = z) -> a, b e. F -> a, b2 e. F -> b = b2
16 15 ealde 
G /\ x = a -> A. y A. z (x, y e. F -> x, z e. F -> y = z) -> a, b e. F -> a, b2 e. F -> b = b2
17 16 ealde 
G -> A. x A. y A. z (x, y e. F -> x, z e. F -> y = z) -> a, b e. F -> a, b2 e. F -> b = b2
18 17 conv isfun 
G -> isfun F -> a, b e. F -> a, b2 e. F -> b = b2
19 3, 18 mpd 
G -> a, b e. F -> a, b2 e. F -> b = b2
20 2, 19 mpd 
G -> a, b2 e. F -> b = b2
21 1, 20 mpd 
G -> b = b2

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 (peano2, addeq, muleq)