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  3638  elrabf  3652  sbcel12  4370  rabxfrd  5367  ffnfvf  7074  nfixpw  8866  mptelixpg  8885  fsumsplit1  15687  ptcldmpt  23477  prdsdsf  24231  prdsxmet  24233  ssiun2sf  32461  iinabrex  32471  acunirnmpt2  32557  acunirnmpt2f  32558  aciunf1lem  32559  funcnv4mpt  32566  fsumiunle  32727  zarclsiin  33834  esumc  34014  esumrnmpt2  34031  esumgect  34053  esum2dlem  34055  esum2d  34056  esumiun  34057  ldsysgenld  34123  sigapildsys  34125  fiunelros  34137  omssubadd  34264  breprexplema  34594  bnj1491  35020  currysetlem  36906  currysetlem1  36908  ptrest  37586  aomclem8  43023  ss2iundf  43621  elunif  44983  rspcegf  44990  fiiuncl  45032  eliuniincex  45076  disjf1  45150  disjf1o  45158  iunmapsn  45184  fmptf  45206  infnsuprnmpt  45217  fmptff  45236  iuneqfzuzlem  45303  allbutfi  45362  supminfrnmpt  45414  supminfxrrnmpt  45440  monoordxr  45451  monoord2xr  45453  iooiinicc  45513  iooiinioc  45527  fsumiunss  45546  fprodcn  45571  climsuse  45579  climsubmpt  45631  climreclf  45635  fnlimcnv  45638  climeldmeqmpt  45639  climfveqmpt  45642  fnlimfvre  45645  fnlimabslt  45650  climfveqmpt3  45653  climbddf  45658  climeldmeqmpt3  45660  climinf2mpt  45685  climinfmpt  45686  limsupequzmptf  45702  lmbr3  45718  fprodcncf  45871  dvmptmulf  45908  dvnmptdivc  45909  dvnmul  45914  dvmptfprodlem  45915  dvnprodlem2  45918  stoweidlem59  46030  fourierdlem31  46109  sge00  46347  sge0pnffigt  46367  sge0lefi  46369  sge0resplit  46377  sge0lempt  46381  sge0iunmptlemfi  46384  sge0iunmptlemre  46386  sge0iunmpt  46389  sge0xadd  46406  sge0gtfsumgt  46414  iundjiun  46431  meadjiun  46437  meaiininclem  46457  omeiunltfirp  46490  hoidmvlelem1  46566  hoidmvlelem3  46568  hspdifhsp  46587  hoiqssbllem2  46594  hspmbllem2  46598  opnvonmbllem2  46604  hoimbl2  46636  vonhoire  46643  iinhoiicc  46645  iunhoiioo  46647  vonn0ioo2  46661  vonn0icc2  46663  incsmflem  46712  issmfle  46716  issmfgt  46727  decsmflem  46737  issmfge  46741  smflimlem2  46743  smflim  46748  smfresal  46759  smfpimbor1lem2  46770  smflim2  46777  smflimmpt  46781  smfsuplem1  46782  smfsupxr  46787  smfinflem  46788  smflimsuplem7  46797  smflimsuplem8  46798  smflimsup  46799  smflimsupmpt  46800  smfliminf  46802  smfliminfmpt  46803  nfdfat  47101