Theorem apprlamed1 ≪ | index | src | ≫ 

theorem apprlamed1 (G P: wff) (a c f: nat) {x: nat} (b: nat x):
  $ G -> c e. a $ >
  $ G /\ x = c -> f @ c = b -> P $ >
  $ G -> f = \. x e. a, b -> P $;
StepHypRefExpression
1 ax_6 
E. x x = c
2 nfv 
F/ x G
3 nfnv 
FN/ x a
4 3 nfrlam1 
FN/ x \. x e. a, b
5 4 nfeq2 
F/ x f = \. x e. a, b
6 nfv 
F/ x P
7 5, 6 nfim 
F/ x f = \. x e. a, b -> P
8 appneq1 
f = \. x e. a, b -> f @ c = (\. x e. a, b) @ c
9 8 eqeq1d 
f = \. x e. a, b -> (f @ c = b <-> (\. x e. a, b) @ c = b)
10 anr 
G /\ x = c -> x = c
11 10 appeq2d 
G /\ x = c -> (\. x e. a, b) @ x = (\. x e. a, b) @ c
12 apprlam 
x e. a -> (\. x e. a, b) @ x = b
13 10 eleq1d 
G /\ x = c -> (x e. a <-> c e. a)
14 hyp h 
G -> c e. a
15 14 anwl 
G /\ x = c -> c e. a
16 13, 15 mpbird 
G /\ x = c -> x e. a
17 12, 16 syl 
G /\ x = c -> (\. x e. a, b) @ x = b
18 11, 17 eqtr3d 
G /\ x = c -> (\. x e. a, b) @ c = b
19 9, 18 syl5ibrcom 
G /\ x = c -> f = \. x e. a, b -> f @ c = b
20 hyp e 
G /\ x = c -> f @ c = b -> P
21 19, 20 syld 
G /\ x = c -> f = \. x e. a, b -> P
22 21 exp 
G -> x = c -> f = \. x e. a, b -> P
23 2, 7, 22 eexdh 
G -> E. x x = c -> f = \. x e. a, b -> P
24 1, 23 mpi 
G -> f = \. x e. a, b -> 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)