Theorem nfel ≪ | index | src | ≫ 

theorem nfel {x: nat} (a: nat x) (A: set x):
  $ FN/ x a $ >
  $ FS/ x A $ >
  $ F/ x a e. A $;
StepHypRefExpression
1 bicom 
(E. y (y = a /\ y e. A) <-> a e. A) -> (a e. A <-> E. y (y = a /\ y e. A))
2 eleq1 
y = a -> (y e. A <-> a e. A)
3 2 exeqe 
E. y (y = a /\ y e. A) <-> a e. A
4 1, 3 ax_mp 
a e. A <-> E. y (y = a /\ y e. A)
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 e. A) -> (F/ x y e. A)
10 hyp h2 
FS/ x A
11 10 conv nfs 
A. y (F/ x y e. A)
12 9, 11 ax_mp 
F/ x y e. A
13 8, 12 nfan 
F/ x y = a /\ y e. A
14 13 nfex 
F/ x E. y (y = a /\ y e. A)
15 4, 14 nfx 
F/ x a e. 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 (ax_8)