Theorem nfel 2906

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-clel 2803  df-nfc 2878

This theorem is referenced by:  nfel1  2908  nfel2  2910  nfnel  3037  elabgf  3641  elrabf  3655  sbcel12  4374  rabxfrd  5372  ffnfvf  7092  nfixpw  8889  mptelixpg  8908  fsumsplit1  15711  ptcldmpt  23501  prdsdsf  24255  prdsxmet  24257  ssiun2sf  32488  iinabrex  32498  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1lem  32586  funcnv4mpt  32593  fsumiunle  32754  zarclsiin  33861  esumc  34041  esumrnmpt2  34058  esumgect  34080  esum2dlem  34082  esum2d  34083  esumiun  34084  ldsysgenld  34150  sigapildsys  34152  fiunelros  34164  omssubadd  34291  breprexplema  34621  bnj1491  35047  currysetlem  36933  currysetlem1  36935  ptrest  37613  aomclem8  43050  ss2iundf  43648  elunif  45010  rspcegf  45017  fiiuncl  45059  eliuniincex  45103  disjf1  45177  disjf1o  45185  iunmapsn  45211  fmptf  45233  infnsuprnmpt  45244  fmptff  45263  iuneqfzuzlem  45330  allbutfi  45389  supminfrnmpt  45441  supminfxrrnmpt  45467  monoordxr  45478  monoord2xr  45480  iooiinicc  45540  iooiinioc  45554  fsumiunss  45573  fprodcn  45598  climsuse  45606  climsubmpt  45658  climreclf  45662  fnlimcnv  45665  climeldmeqmpt  45666  climfveqmpt  45669  fnlimfvre  45672  fnlimabslt  45677  climfveqmpt3  45680  climbddf  45685  climeldmeqmpt3  45687  climinf2mpt  45712  climinfmpt  45713  limsupequzmptf  45729  lmbr3  45745  fprodcncf  45898  dvmptmulf  45935  dvnmptdivc  45936  dvnmul  45941  dvmptfprodlem  45942  dvnprodlem2  45945  stoweidlem59  46057  fourierdlem31  46136  sge00  46374  sge0pnffigt  46394  sge0lefi  46396  sge0resplit  46404  sge0lempt  46408  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0xadd  46433  sge0gtfsumgt  46441  iundjiun  46458  meadjiun  46464  meaiininclem  46484  omeiunltfirp  46517  hoidmvlelem1  46593  hoidmvlelem3  46595  hspdifhsp  46614  hoiqssbllem2  46621  hspmbllem2  46625  opnvonmbllem2  46631  hoimbl2  46663  vonhoire  46670  iinhoiicc  46672  iunhoiioo  46674  vonn0ioo2  46688  vonn0icc2  46690  incsmflem  46739  issmfle  46743  issmfgt  46754  decsmflem  46764  issmfge  46768  smflimlem2  46770  smflim  46775  smfresal  46786  smfpimbor1lem2  46797  smflim2  46804  smflimmpt  46808  smfsuplem1  46809  smfsupxr  46814  smfinflem  46815  smflimsuplem7  46824  smflimsuplem8  46825  smflimsup  46826  smflimsupmpt  46827  smfliminf  46829  smfliminfmpt  46830  nfdfat  47128