Theorem rappsabed1 ≪ | index | src | ≫ 

theorem rappsabed1 (F: set) (G P: wff) (a: nat) {x: nat} (A: set x):
  $ G /\ x = a -> F @' a == A -> P $ >
  $ G -> F == S\ x, A -> P $;
StepHypRefExpression
1 ax_6 
E. x x = a
2 nfv 
F/ x G
3 nfsv 
FS/ x F
4 nfsab1 
FS/ x S\ x, A
5 3, 4 nfeqs 
F/ x F == S\ x, A
6 nfv 
F/ x P
7 5, 6 nfim 
F/ x F == S\ x, A -> P
8 rappeq1 
F == S\ x, A -> F @' a == (S\ x, A) @' a
9 8 eqseq1d 
F == S\ x, A -> (F @' a == A <-> (S\ x, A) @' a == A)
10 rappsab 
(S\ x, A) @' x == A
11 anr 
G /\ x = a -> x = a
12 11 rappeq2d 
G /\ x = a -> (S\ x, A) @' x == (S\ x, A) @' a
13 12 eqscomd 
G /\ x = a -> (S\ x, A) @' a == (S\ x, A) @' x
14 10, 13 syl6eqs 
G /\ x = a -> (S\ x, A) @' a == A
15 9, 14 syl5ibrcom 
G /\ x = a -> F == S\ x, A -> F @' a == A
16 hyp e 
G /\ x = a -> F @' a == A -> P
17 15, 16 syld 
G /\ x = a -> F == S\ x, A -> P
18 17 exp 
G -> x = a -> F == S\ x, A -> P
19 2, 7, 18 eexdh 
G -> E. x x = a -> F == S\ x, A -> P
20 1, 19 mpi 
G -> F == S\ x, A -> P

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)