Theorem nfel 2914

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 2911	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 ∈ 𝐵)
6	5	mptru 1549	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-clel 2812  df-nfc 2886

This theorem is referenced by:  nfel1  2916  nfel2  2918  nfnel  3045  elabgf  3618  elrabf  3632  sbcel12  4352  rabxfrd  5352  ffnfvf  7064  nfixpw  8855  mptelixpg  8874  fsumsplit1  15696  ptcldmpt  23588  prdsdsf  24341  prdsxmet  24343  ssiun2sf  32649  iinabrex  32659  acunirnmpt2  32753  acunirnmpt2f  32754  aciunf1lem  32755  funcnv4mpt  32761  fsumiunle  32922  zarclsiin  34036  esumc  34216  esumrnmpt2  34233  esumgect  34255  esum2dlem  34257  esum2d  34258  esumiun  34259  ldsysgenld  34325  sigapildsys  34327  fiunelros  34339  omssubadd  34465  breprexplema  34795  bnj1491  35220  currysetlem  37265  currysetlem1  37267  ptrest  37951  aomclem8  43504  ss2iundf  44101  elunif  45462  rspcegf  45469  fiiuncl  45511  eliuniincex  45554  disjf1  45628  disjf1o  45636  iunmapsn  45661  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  47572