Theorem nfel 2777

Description: Hypothesis builder for elementhood. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

Hypotheses

Ref	Expression
nfnfc.1	|- F/_ x A
nfeq.2	|- F/_ x B

Assertion

Ref	Expression
nfel	|- F/ x A e. B

Proof of Theorem nfel

Step	Hyp	Ref	Expression
1		nfnfc.1	. . . 4 |- F/_ x A
2	1	a1i 11	. . 3 |- ( T. -> F/_ x A )
3		nfeq.2	. . . 4 |- F/_ x B
4	3	a1i 11	. . 3 |- ( T. -> F/_ x B )
5	2, 4	nfeld 2773	. 2 |- ( T. -> F/ x A e. B )
6	5	trud 1493	1 |- F/ x A e. B

Syntax hints:   T. wtru 1484   F/wnf 1708   e. wcel 1990   F/_wnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753

This theorem is referenced by:  nfel1  2779  nfel2  2781  nfnel  2904  elabgf  3348  elrabf  3360  sbcel12  3983  rabxfrd  4889  ffnfvf  6389  mptelixpg  7945  ac6num  9301  fproddivf  14718  fprodsplit1f  14721  ptcldmpt  21417  prdsdsf  22172  prdsxmet  22174  rmo4fOLD  29336  ssiun2sf  29378  acunirnmpt2  29460  acunirnmpt2f  29461  aciunf1lem  29462  funcnv4mpt  29470  fsumiunle  29575  esumc  30113  esumrnmpt2  30130  esumgect  30152  esum2dlem  30154  esum2d  30155  esumiun  30156  ldsysgenld  30223  sigapildsys  30225  fiunelros  30237  omssubadd  30362  breprexplema  30708  bnj1491  31125  ptrest  33408  aomclem8  37631  ss2iundf  37951  sbcel12gOLD  38754  elunif  39175  rspcegf  39182  fiiuncl  39234  cbvmpt21  39278  eliuniincex  39292  iinssiin  39312  iinssf  39327  disjf1  39369  wessf1ornlem  39371  disjrnmpt2  39375  disjf1o  39378  disjinfi  39380  iunmapsn  39409  fmptf  39448  infnsuprnmpt  39465  iuneqfzuzlem  39550  allbutfi  39616  supminfrnmpt  39672  supminfxrrnmpt  39701  iooiinicc  39769  iooiinioc  39783  fsumsplit1  39804  fsumiunss  39807  fprodcnlem  39831  fprodcn  39832  climsuse  39840  climsubmpt  39892  climreclf  39896  fnlimcnv  39899  climeldmeqmpt  39900  climfveqmpt  39903  fnlimfvre  39906  fnlimabslt  39911  climfveqmpt3  39914  climbddf  39919  climeldmeqmpt3  39921  climinf2mpt  39946  climinfmpt  39947  limsupequzmptf  39963  lmbr3  39979  fprodcncf  40114  dvmptmulf  40152  dvnmptdivc  40153  dvnmul  40158  dvmptfprodlem  40159  dvmptfprod  40160  dvnprodlem1  40161  dvnprodlem2  40162  stoweidlem59  40276  fourierdlem31  40355  sge00  40593  sge0f1o  40599  sge0pnffigt  40613  sge0lefi  40615  sge0resplit  40623  sge0lempt  40627  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0xadd  40652  sge0gtfsumgt  40660  iundjiun  40677  meadjiun  40683  meaiininclem  40700  omeiunltfirp  40733  hoidmvlelem1  40809  hoidmvlelem3  40811  hspdifhsp  40830  hoiqssbllem2  40837  hspmbllem2  40841  opnvonmbllem2  40847  hoimbl2  40879  vonhoire  40886  iinhoiicc  40888  iunhoiioo  40890  vonn0ioo2  40904  vonn0icc2  40906  incsmflem  40950  issmfle  40954  issmfgt  40965  decsmflem  40974  issmfge  40978  smflimlem2  40980  smflim  40985  smfresal  40995  smfpimbor1lem2  41006  smflim2  41012  smflimmpt  41016  smfsuplem1  41017  smfsupmpt  41021  smfsupxr  41022  smfinflem  41023  smfinfmpt  41025  smflimsuplem7  41032  smflimsuplem8  41033  smflimsup  41034  smflimsupmpt  41035  smfliminf  41037  smfliminfmpt  41038  nfdfat  41210