Theorem nfeld 2627

Description: Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)

Hypotheses

Ref	Expression
nfeqd.1
nfeqd.2

Assertion

Ref	Expression
nfeld

Proof of Theorem nfeld

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-clel 2452	. 2
2		nfv 1707	. . 3
3		nfcvd 2620	. . . . 5
4		nfeqd.1	. . . . 5
5	3, 4	nfeqd 2626	. . . 4
6		nfeqd.2	. . . . 5
7	6	nfcrd 2625	. . . 4
8	5, 7	nfand 1925	. . 3
9	2, 8	nfexd 1952	. 2
10	1, 9	nfxfrd 1646	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  E.wex 1612  F/wnf 1616  e.wcel 1818  F/_wnfc 2605

This theorem is referenced by:  nfel  2632  nfneld  2801  nfrald  2842  ralcom2  3022  nfreud  3030  nfrmod  3031  nfrmo  3033  nfsbc1d  3345  nfsbcd  3348  sbcrextOLD  3409  sbcrext  3410  nfdisj  4434  nfbrd  4495  nfriotad  6265  nfixp  7508  axrepndlem2  8989  axrepnd  8990  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axpownd  8999  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607