Theorem subsni ≪ | index | src | ≫ 

theorem subsni (A: set) (G: wff) (a b: nat):
  $ G -> subsn A $ >
  $ G -> a e. A $ >
  $ G -> b e. A $ >
  $ G -> a = b $;
StepHypRefExpression
1 hyp h2 
G -> b e. A
2 hyp h1 
G -> a e. A
3 hyp h 
G -> subsn A
4 anlr 
G /\ x = a /\ y = b -> x = a
5 4 eleq1d 
G /\ x = a /\ y = b -> (x e. A <-> a e. A)
6 anr 
G /\ x = a /\ y = b -> y = b
7 6 eleq1d 
G /\ x = a /\ y = b -> (y e. A <-> b e. A)
8 4, 6 eqeqd 
G /\ x = a /\ y = b -> (x = y <-> a = b)
9 7, 8 imeqd 
G /\ x = a /\ y = b -> (y e. A -> x = y <-> b e. A -> a = b)
10 5, 9 imeqd 
G /\ x = a /\ y = b -> (x e. A -> y e. A -> x = y <-> a e. A -> b e. A -> a = b)
11 10 bi1d 
G /\ x = a /\ y = b -> (x e. A -> y e. A -> x = y) -> a e. A -> b e. A -> a = b
12 11 ealde 
G /\ x = a -> A. y (x e. A -> y e. A -> x = y) -> a e. A -> b e. A -> a = b
13 12 ealde 
G -> A. x A. y (x e. A -> y e. A -> x = y) -> a e. A -> b e. A -> a = b
14 13 conv subsn 
G -> subsn A -> a e. A -> b e. A -> a = b
15 3, 14 mpd 
G -> a e. A -> b e. A -> a = b
16 2, 15 mpd 
G -> b e. A -> a = b
17 1, 16 mpd 
G -> a = b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_12), axs_set (ax_8)