Theorem nfel 2913

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785   ∈ wcel 2114  Ⅎ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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2728  df-clel 2811  df-nfc 2885

This theorem is referenced by:  nfel1  2915  nfel2  2917  nfnel  3044  elabgf  3617  elrabf  3631  sbcel12  4351  rabxfrd  5359  ffnfvf  7072  nfixpw  8864  mptelixpg  8883  fsumsplit1  15707  ptcldmpt  23579  prdsdsf  24332  prdsxmet  24334  ssiun2sf  32629  iinabrex  32639  acunirnmpt2  32733  acunirnmpt2f  32734  aciunf1lem  32735  funcnv4mpt  32741  fsumiunle  32902  zarclsiin  34015  esumc  34195  esumrnmpt2  34212  esumgect  34234  esum2dlem  34236  esum2d  34237  esumiun  34238  ldsysgenld  34304  sigapildsys  34306  fiunelros  34318  omssubadd  34444  breprexplema  34774  bnj1491  35199  currysetlem  37252  currysetlem1  37254  ptrest  37940  aomclem8  43489  ss2iundf  44086  elunif  45447  rspcegf  45454  fiiuncl  45496  eliuniincex  45539  disjf1  45613  disjf1o  45621  iunmapsn  45646  fmptf  45668  infnsuprnmpt  45679  fmptff  45698  iuneqfzuzlem  45764  allbutfi  45822  supminfrnmpt  45873  supminfxrrnmpt  45899  monoordxr  45910  monoord2xr  45912  iooiinicc  45972  iooiinioc  45986  fsumiunss  46005  fprodcn  46030  climsuse  46038  climsubmpt  46088  climreclf  46092  fnlimcnv  46095  climeldmeqmpt  46096  climfveqmpt  46099  fnlimfvre  46102  fnlimabslt  46107  climfveqmpt3  46110  climbddf  46115  climeldmeqmpt3  46117  climinf2mpt  46142  climinfmpt  46143  limsupequzmptf  46159  lmbr3  46175  fprodcncf  46328  dvmptmulf  46365  dvnmptdivc  46366  dvnmul  46371  dvmptfprodlem  46372  dvnprodlem2  46375  stoweidlem59  46487  fourierdlem31  46566  sge00  46804  sge0pnffigt  46824  sge0lefi  46826  sge0resplit  46834  sge0lempt  46838  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0xadd  46863  sge0gtfsumgt  46871  iundjiun  46888  meadjiun  46894  meaiininclem  46914  omeiunltfirp  46947  hoidmvlelem1  47023  hoidmvlelem3  47025  hspdifhsp  47044  hoiqssbllem2  47051  hspmbllem2  47055  opnvonmbllem2  47061  hoimbl2  47093  vonhoire  47100  iinhoiicc  47102  iunhoiioo  47104  vonn0ioo2  47118  vonn0icc2  47120  incsmflem  47169  issmfle  47173  issmfgt  47184  decsmflem  47194  issmfge  47198  smflimlem2  47200  smflim  47205  smfresal  47216  smfpimbor1lem2  47227  smflim2  47234  smflimmpt  47238  smfsuplem1  47239  smfsupxr  47244  smfinflem  47245  smflimsuplem7  47254  smflimsuplem8  47255  smflimsup  47256  smflimsupmpt  47257  smfliminf  47259  smfliminfmpt  47260  nfdfat  47575