Theorem nfthe ≪ | index | src | ≫ 

theorem nfthe {x: nat} (A: set x): $ FS/ x A $ > $ FN/ x the A $;
StepHypRefExpression
1 eqtheb 
y = the A <-> A == {u | u = y} \/ ~E. v A == {u | u = v} /\ y = 0
2 hyp h 
FS/ x A
3 nfsv 
FS/ x {u | u = y}
4 2, 3 nfeqs 
F/ x A == {u | u = y}
5 nfsv 
FS/ x {u | u = v}
6 2, 5 nfeqs 
F/ x A == {u | u = v}
7 6 nfex 
F/ x E. v A == {u | u = v}
8 7 nfnot 
F/ x ~E. v A == {u | u = v}
9 nfv 
F/ x y = 0
10 8, 9 nfan 
F/ x ~E. v A == {u | u = v} /\ y = 0
11 4, 10 nfor 
F/ x A == {u | u = y} \/ ~E. v A == {u | u = v} /\ y = 0
12 1, 11 nfx 
F/ x y = the A
13 12 nfnri 
FN/ x the A

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)