Theorem nfel 2917

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1785   ∈ wcel 2106  Ⅎwnfc 2883

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-cleq 2724  df-clel 2810  df-nfc 2885

This theorem is referenced by:  nfel1  2919  nfel2  2921  nfnel  3054  elabgf  3663  elrabf  3678  sbcel12  4407  rabxfrd  5414  ffnfvf  7115  nfixpw  8906  mptelixpg  8925  fsumsplit1  15687  ptcldmpt  23109  prdsdsf  23864  prdsxmet  23866  ssiun2sf  31778  iinabrex  31787  acunirnmpt2  31872  acunirnmpt2f  31873  aciunf1lem  31874  funcnv4mpt  31881  fsumiunle  32022  zarclsiin  32839  esumc  33037  esumrnmpt2  33054  esumgect  33076  esum2dlem  33078  esum2d  33079  esumiun  33080  ldsysgenld  33146  sigapildsys  33148  fiunelros  33160  omssubadd  33287  breprexplema  33630  bnj1491  34056  currysetlem  35814  currysetlem1  35816  ptrest  36475  aomclem8  41788  ss2iundf  42395  elunif  43685  rspcegf  43692  fiiuncl  43737  eliuniincex  43783  disjf1  43865  disjf1o  43874  iunmapsn  43901  fmptf  43927  infnsuprnmpt  43940  fmptff  43960  iuneqfzuzlem  44030  allbutfi  44089  supminfrnmpt  44141  supminfxrrnmpt  44167  monoordxr  44179  monoord2xr  44181  iooiinicc  44241  iooiinioc  44255  fsumiunss  44277  fprodcnlem  44301  fprodcn  44302  climsuse  44310  climsubmpt  44362  climreclf  44366  fnlimcnv  44369  climeldmeqmpt  44370  climfveqmpt  44373  fnlimfvre  44376  fnlimabslt  44381  climfveqmpt3  44384  climbddf  44389  climeldmeqmpt3  44391  climinf2mpt  44416  climinfmpt  44417  limsupequzmptf  44433  lmbr3  44449  fprodcncf  44602  dvmptmulf  44639  dvnmptdivc  44640  dvnmul  44645  dvmptfprodlem  44646  dvmptfprod  44647  dvnprodlem1  44648  dvnprodlem2  44649  stoweidlem59  44761  fourierdlem31  44840  sge00  45078  sge0f1o  45084  sge0pnffigt  45098  sge0lefi  45100  sge0resplit  45108  sge0lempt  45112  sge0iunmptlemfi  45115  sge0iunmptlemre  45117  sge0iunmpt  45120  sge0xadd  45137  sge0gtfsumgt  45145  iundjiun  45162  meadjiun  45168  meaiininclem  45188  omeiunltfirp  45221  hoidmvlelem1  45297  hoidmvlelem3  45299  hspdifhsp  45318  hoiqssbllem2  45325  hspmbllem2  45329  opnvonmbllem2  45335  hoimbl2  45367  vonhoire  45374  iinhoiicc  45376  iunhoiioo  45378  vonn0ioo2  45392  vonn0icc2  45394  incsmflem  45443  issmfle  45447  issmfgt  45458  decsmflem  45468  issmfge  45472  smflimlem2  45474  smflim  45479  smfresal  45490  smfpimbor1lem2  45501  smflim2  45508  smflimmpt  45512  smfsuplem1  45513  smfsupxr  45518  smfinflem  45519  smfinfmpt  45521  smflimsuplem7  45528  smflimsuplem8  45529  smflimsup  45530  smflimsupmpt  45531  smfliminf  45533  smfliminfmpt  45534  nfdfat  45821