Theorem nfel 2939

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

Syntax hints:  ⊤wtru 1571  Ⅎwnf 1813   ∈ wcel 2143  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-cleq 2755  df-clel 2838  df-nfc 2912

This theorem is referenced by:  nfel1  2941  nfel2  2943  nfnel  3072  elabgf  3634  elrabf  3648  sbcel12  4377  rabxfrd  5390  ffnfvf  7117  nfixpw  8915  mptelixpg  8934  fsumsplit1  15798  ptcldmpt  23752  prdsdsf  24505  prdsxmet  24507  ssiun2sf  32885  iinabrex  32895  acunirnmpt2  32986  acunirnmpt2f  32987  aciunf1lem  32988  funcnv4mpt  32994  fsumiunle  33154  zarclsiin  34242  esumc  34422  esumrnmpt2  34439  esumgect  34461  esum2dlem  34463  esum2d  34464  esumiun  34465  ldsysgenld  34531  sigapildsys  34533  fiunelros  34545  omssubadd  34671  breprexplema  34998  bnj1491  35426  currysetlem  37562  currysetlem1  37564  ptrest  38251  aomclem8  43771  ss2iundf  44368  elunif  45719  rspcegf  45726  fiiuncl  45768  eliuniincex  45810  disjf1  45884  disjf1o  45892  iunmapsn  45916  fmptf  45937  infnsuprnmpt  45948  fmptff  45967  iuneqfzuzlem  46033  allbutfi  46091  supminfrnmpt  46142  supminfxrrnmpt  46168  monoordxr  46179  monoord2xr  46181  iooiinicc  46241  iooiinioc  46255  fsumiunss  46274  fprodcn  46299  climsuse  46307  climsubmpt  46357  climreclf  46361  fnlimcnv  46364  climeldmeqmpt  46365  climfveqmpt  46368  fnlimfvre  46371  fnlimabslt  46376  climfveqmpt3  46379  climbddf  46384  climeldmeqmpt3  46386  climinf2mpt  46411  climinfmpt  46412  limsupequzmptf  46428  lmbr3  46444  fprodcncf  46597  dvmptmulf  46634  dvnmptdivc  46635  dvnmul  46640  dvmptfprodlem  46641  dvnprodlem2  46644  stoweidlem59  46756  fourierdlem31  46835  sge00  47073  sge0pnffigt  47093  sge0lefi  47095  sge0resplit  47103  sge0lempt  47107  sge0iunmptlemfi  47110  sge0iunmptlemre  47112  sge0iunmpt  47115  sge0xadd  47132  sge0gtfsumgt  47140  iundjiun  47157  meadjiun  47163  meaiininclem  47183  omeiunltfirp  47216  hoidmvlelem1  47292  hoidmvlelem3  47294  hspdifhsp  47313  hoiqssbllem2  47320  hspmbllem2  47324  opnvonmbllem2  47330  hoimbl2  47362  vonhoire  47369  iinhoiicc  47371  iunhoiioo  47373  vonn0ioo2  47387  vonn0icc2  47389  incsmflem  47438  issmfle  47442  issmfgt  47453  decsmflem  47463  issmfge  47467  smflimlem2  47469  smflim  47474  smfresal  47485  smfpimbor1lem2  47496  smflim2  47503  smflimmpt  47507  smfsuplem1  47508  smfsupxr  47513  smfinflem  47514  smflimsuplem7  47523  smflimsuplem8  47524  smflimsup  47525  smflimsupmpt  47526  smfliminf  47528  smfliminfmpt  47529  nfdfat  47847