Theorem applamed1 ≪ | index | src | ≫ 

theorem applamed1 (F: set) (G P: wff) (b: nat) {x: nat} (a: nat x):
  $ G /\ x = b -> F @ b = a -> P $ >
  $ G -> F == \ x, a -> P $;
StepHypRefExpression
1 ax_6 
E. x x = b
2 nfv 
F/ x G
3 nfsv 
FS/ x F
4 nflam1 
FS/ x \ x, a
5 3, 4 nfeqs 
F/ x F == \ x, a
6 nfv 
F/ x P
7 5, 6 nfim 
F/ x F == \ x, a -> P
8 appeq1 
F == \ x, a -> F @ b = (\ x, a) @ b
9 8 eqeq1d 
F == \ x, a -> (F @ b = a <-> (\ x, a) @ b = a)
10 applam 
(\ x, a) @ x = a
11 anr 
G /\ x = b -> x = b
12 11 appeq2d 
G /\ x = b -> (\ x, a) @ x = (\ x, a) @ b
13 12 eqcomd 
G /\ x = b -> (\ x, a) @ b = (\ x, a) @ x
14 10, 13 syl6eq 
G /\ x = b -> (\ x, a) @ b = a
15 9, 14 syl5ibrcom 
G /\ x = b -> F == \ x, a -> F @ b = a
16 hyp e 
G /\ x = b -> F @ b = a -> P
17 15, 16 syld 
G /\ x = b -> F == \ x, a -> P
18 17 exp 
G -> x = b -> F == \ x, a -> P
19 2, 7, 18 eexdh 
G -> E. x x = b -> F == \ x, a -> P
20 1, 19 mpi 
G -> F == \ 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)