Theorem rappslamed ≪ | index | src | ≫ 

theorem rappslamed (C: set) (G: wff) (a b: nat) {x: nat} (A: set x):
  $ G /\ x = a -> A @' b == C $ >
  $ G -> (\\ x, A) @' (a, b) == C $;
StepHypRefExpression
1 rappslams 
(\\ x, A) @' (a, b) == (S[a / x] A) @' b
2 ax_6 
E. x x = a
3 nfv 
F/ x G
4 nfsbs1 
FS/ x S[a / x] A
5 nfnv 
FN/ x b
6 4, 5 nfrapp 
FS/ x (S[a / x] A) @' b
7 nfsv 
FS/ x C
8 6, 7 nfeqs 
F/ x (S[a / x] A) @' b == C
9 sbsq 
x = a -> A == S[a / x] A
10 9 anwr 
G /\ x = a -> A == S[a / x] A
11 10 rappeq1d 
G /\ x = a -> A @' b == (S[a / x] A) @' b
12 hyp h 
G /\ x = a -> A @' b == C
13 11, 12 eqstr3d 
G /\ x = a -> (S[a / x] A) @' b == C
14 13 exp 
G -> x = a -> (S[a / x] A) @' b == C
15 3, 8, 14 eexdh 
G -> E. x x = a -> (S[a / x] A) @' b == C
16 2, 15 mpi 
G -> (S[a / x] A) @' b == C
17 1, 16 syl5eqs 
G -> (\\ x, A) @' (a, b) == C

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)