Theorem nfel 2945

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

Syntax hints:  ⊤wtru 1568  Ⅎwnf 1810   ∈ wcel 2149  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-cleq 2761  df-clel 2844  df-nfc 2918

This theorem is referenced by:  nfel1  2947  nfel2  2949  nfnel  3078  elabgf  3642  elrabf  3656  sbcel12  4374  rabxfrd  5386  ffnfvf  7113  nfixpw  8910  mptelixpg  8929  fsumsplit1  15792  ptcldmpt  23736  prdsdsf  24489  prdsxmet  24491  ssiun2sf  32841  iinabrex  32851  acunirnmpt2  32942  acunirnmpt2f  32943  aciunf1lem  32944  funcnv4mpt  32950  fsumiunle  33110  zarclsiin  34202  esumc  34382  esumrnmpt2  34399  esumgect  34421  esum2dlem  34423  esum2d  34424  esumiun  34425  ldsysgenld  34491  sigapildsys  34493  fiunelros  34505  omssubadd  34631  breprexplema  34958  bnj1491  35386  currysetlem  37465  currysetlem1  37467  ptrest  38153  aomclem8  43673  ss2iundf  44270  elunif  45621  rspcegf  45628  fiiuncl  45670  eliuniincex  45712  disjf1  45786  disjf1o  45794  iunmapsn  45818  fmptf  45839  infnsuprnmpt  45850  fmptff  45869  iuneqfzuzlem  45935  allbutfi  45993  supminfrnmpt  46044  supminfxrrnmpt  46070  monoordxr  46081  monoord2xr  46083  iooiinicc  46143  iooiinioc  46157  fsumiunss  46176  fprodcn  46201  climsuse  46209  climsubmpt  46259  climreclf  46263  fnlimcnv  46266  climeldmeqmpt  46267  climfveqmpt  46270  fnlimfvre  46273  fnlimabslt  46278  climfveqmpt3  46281  climbddf  46286  climeldmeqmpt3  46288  climinf2mpt  46313  climinfmpt  46314  limsupequzmptf  46330  lmbr3  46346  fprodcncf  46499  dvmptmulf  46536  dvnmptdivc  46537  dvnmul  46542  dvmptfprodlem  46543  dvnprodlem2  46546  stoweidlem59  46658  fourierdlem31  46737  sge00  46975  sge0pnffigt  46995  sge0lefi  46997  sge0resplit  47005  sge0lempt  47009  sge0iunmptlemfi  47012  sge0iunmptlemre  47014  sge0iunmpt  47017  sge0xadd  47034  sge0gtfsumgt  47042  iundjiun  47059  meadjiun  47065  meaiininclem  47085  omeiunltfirp  47118  hoidmvlelem1  47194  hoidmvlelem3  47196  hspdifhsp  47215  hoiqssbllem2  47222  hspmbllem2  47226  opnvonmbllem2  47232  hoimbl2  47264  vonhoire  47271  iinhoiicc  47273  iunhoiioo  47275  vonn0ioo2  47289  vonn0icc2  47291  incsmflem  47340  issmfle  47344  issmfgt  47355  decsmflem  47365  issmfge  47369  smflimlem2  47371  smflim  47376  smfresal  47387  smfpimbor1lem2  47398  smflim2  47405  smflimmpt  47409  smfsuplem1  47410  smfsupxr  47415  smfinflem  47416  smflimsuplem7  47425  smflimsuplem8  47426  smflimsup  47427  smflimsupmpt  47428  smfliminf  47430  smfliminfmpt  47431  nfdfat  47746