Theorem nfel 2915

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	⊢ Ⅎ𝑥𝐴
nfeq.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfel	⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Proof of Theorem nfel

Step	Hyp	Ref	Expression
1		nfnfc.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfeq.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
5	2, 4	nfeld 2912	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 ∈ 𝐵)
6	5	mptru 1554	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  ⊤wtru 1548  Ⅎwnf 1790   ∈ wcel 2119  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-cleq 2731  df-clel 2814  df-nfc 2888

This theorem is referenced by:  nfel1  2917  nfel2  2919  nfnel  3046  elabgf  3612  elrabf  3626  sbcel12  4339  rabxfrd  5346  ffnfvf  7061  nfixpw  8854  mptelixpg  8873  fsumsplit1  15698  ptcldmpt  23597  prdsdsf  24350  prdsxmet  24352  ssiun2sf  32648  iinabrex  32658  acunirnmpt2  32752  acunirnmpt2f  32753  aciunf1lem  32754  funcnv4mpt  32760  fsumiunle  32921  zarclsiin  34055  esumc  34235  esumrnmpt2  34252  esumgect  34274  esum2dlem  34276  esum2d  34277  esumiun  34278  ldsysgenld  34344  sigapildsys  34346  fiunelros  34358  omssubadd  34484  breprexplema  34814  bnj1491  35239  currysetlem  37298  currysetlem1  37300  ptrest  37986  aomclem8  43506  ss2iundf  44103  elunif  45464  rspcegf  45471  fiiuncl  45513  eliuniincex  45556  disjf1  45630  disjf1o  45638  iunmapsn  45662  fmptf  45683  infnsuprnmpt  45694  fmptff  45713  iuneqfzuzlem  45779  allbutfi  45837  supminfrnmpt  45888  supminfxrrnmpt  45914  monoordxr  45925  monoord2xr  45927  iooiinicc  45987  iooiinioc  46001  fsumiunss  46020  fprodcn  46045  climsuse  46053  climsubmpt  46103  climreclf  46107  fnlimcnv  46110  climeldmeqmpt  46111  climfveqmpt  46114  fnlimfvre  46117  fnlimabslt  46122  climfveqmpt3  46125  climbddf  46130  climeldmeqmpt3  46132  climinf2mpt  46157  climinfmpt  46158  limsupequzmptf  46174  lmbr3  46190  fprodcncf  46343  dvmptmulf  46380  dvnmptdivc  46381  dvnmul  46386  dvmptfprodlem  46387  dvnprodlem2  46390  stoweidlem59  46502  fourierdlem31  46581  sge00  46819  sge0pnffigt  46839  sge0lefi  46841  sge0resplit  46849  sge0lempt  46853  sge0iunmptlemfi  46856  sge0iunmptlemre  46858  sge0iunmpt  46861  sge0xadd  46878  sge0gtfsumgt  46886  iundjiun  46903  meadjiun  46909  meaiininclem  46929  omeiunltfirp  46962  hoidmvlelem1  47038  hoidmvlelem3  47040  hspdifhsp  47059  hoiqssbllem2  47066  hspmbllem2  47070  opnvonmbllem2  47076  hoimbl2  47108  vonhoire  47115  iinhoiicc  47117  iunhoiioo  47119  vonn0ioo2  47133  vonn0icc2  47135  incsmflem  47184  issmfle  47188  issmfgt  47199  decsmflem  47209  issmfge  47213  smflimlem2  47215  smflim  47220  smfresal  47231  smfpimbor1lem2  47242  smflim2  47249  smflimmpt  47253  smfsuplem1  47254  smfsupxr  47259  smfinflem  47260  smflimsuplem7  47269  smflimsuplem8  47270  smflimsup  47271  smflimsupmpt  47272  smfliminf  47274  smfliminfmpt  47275  nfdfat  47590