Theorem nfel 2918

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2725  df-clel 2811  df-nfc 2886

This theorem is referenced by:  nfel1  2920  nfel2  2922  nfnel  3055  elabgf  3665  elrabf  3680  sbcel12  4409  rabxfrd  5416  ffnfvf  7119  nfixpw  8910  mptelixpg  8929  fsumsplit1  15691  ptcldmpt  23118  prdsdsf  23873  prdsxmet  23875  ssiun2sf  31791  iinabrex  31800  acunirnmpt2  31885  acunirnmpt2f  31886  aciunf1lem  31887  funcnv4mpt  31894  fsumiunle  32035  zarclsiin  32851  esumc  33049  esumrnmpt2  33066  esumgect  33088  esum2dlem  33090  esum2d  33091  esumiun  33092  ldsysgenld  33158  sigapildsys  33160  fiunelros  33172  omssubadd  33299  breprexplema  33642  bnj1491  34068  currysetlem  35826  currysetlem1  35828  ptrest  36487  aomclem8  41803  ss2iundf  42410  elunif  43700  rspcegf  43707  fiiuncl  43752  eliuniincex  43798  disjf1  43880  disjf1o  43889  iunmapsn  43916  fmptf  43942  infnsuprnmpt  43954  fmptff  43974  iuneqfzuzlem  44044  allbutfi  44103  supminfrnmpt  44155  supminfxrrnmpt  44181  monoordxr  44193  monoord2xr  44195  iooiinicc  44255  iooiinioc  44269  fsumiunss  44291  fprodcnlem  44315  fprodcn  44316  climsuse  44324  climsubmpt  44376  climreclf  44380  fnlimcnv  44383  climeldmeqmpt  44384  climfveqmpt  44387  fnlimfvre  44390  fnlimabslt  44395  climfveqmpt3  44398  climbddf  44403  climeldmeqmpt3  44405  climinf2mpt  44430  climinfmpt  44431  limsupequzmptf  44447  lmbr3  44463  fprodcncf  44616  dvmptmulf  44653  dvnmptdivc  44654  dvnmul  44659  dvmptfprodlem  44660  dvmptfprod  44661  dvnprodlem1  44662  dvnprodlem2  44663  stoweidlem59  44775  fourierdlem31  44854  sge00  45092  sge0f1o  45098  sge0pnffigt  45112  sge0lefi  45114  sge0resplit  45122  sge0lempt  45126  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0iunmpt  45134  sge0xadd  45151  sge0gtfsumgt  45159  iundjiun  45176  meadjiun  45182  meaiininclem  45202  omeiunltfirp  45235  hoidmvlelem1  45311  hoidmvlelem3  45313  hspdifhsp  45332  hoiqssbllem2  45339  hspmbllem2  45343  opnvonmbllem2  45349  hoimbl2  45381  vonhoire  45388  iinhoiicc  45390  iunhoiioo  45392  vonn0ioo2  45406  vonn0icc2  45408  incsmflem  45457  issmfle  45461  issmfgt  45472  decsmflem  45482  issmfge  45486  smflimlem2  45488  smflim  45493  smfresal  45504  smfpimbor1lem2  45515  smflim2  45522  smflimmpt  45526  smfsuplem1  45527  smfsupxr  45532  smfinflem  45533  smfinfmpt  45535  smflimsuplem7  45542  smflimsuplem8  45543  smflimsup  45544  smflimsupmpt  45545  smfliminf  45547  smfliminfmpt  45548  nfdfat  45835