Theorem nf_eq ≪ | index | src | ≫ 

theorem nf_eq {x: nat} (a b: nat x): $ FN/ x a $ > $ FN/ x b $ > $ F/ x a = b $;
StepHypRefExpression
1 bicom 
(E. y (y = a /\ y = b) <-> a = b) -> (a = b <-> E. y (y = a /\ y = b))
2 eqeq1 
y = a -> (y = b <-> a = b)
3 2 exeqe 
E. y (y = a /\ y = b) <-> a = b
4 1, 3 ax_mp 
a = b <-> E. y (y = a /\ y = b)
5 eal 
A. y (F/ x y = a) -> (F/ x y = a)
6 hyp h1 
FN/ x a
7 6 conv nfn 
A. y (F/ x y = a)
8 5, 7 ax_mp 
F/ x y = a
9 eal 
A. y (F/ x y = b) -> (F/ x y = b)
10 hyp h2 
FN/ x b
11 10 conv nfn 
A. y (F/ x y = b)
12 9, 11 ax_mp 
F/ x y = b
13 8, 12 nfan 
F/ x y = a /\ y = b
14 13 nfex 
F/ x E. y (y = a /\ y = b)
15 4, 14 nfx 
F/ x a = b

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)