Theorem nfel 2920

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783   ∈ wcel 2108  Ⅎwnfc 2890

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-clel 2816  df-nfc 2892

This theorem is referenced by:  nfel1  2922  nfel2  2924  nfnel  3054  elabgf  3674  elrabf  3688  sbcel12  4411  rabxfrd  5417  ffnfvf  7140  nfixpw  8956  mptelixpg  8975  fsumsplit1  15781  ptcldmpt  23622  prdsdsf  24377  prdsxmet  24379  ssiun2sf  32572  iinabrex  32582  acunirnmpt2  32670  acunirnmpt2f  32671  aciunf1lem  32672  funcnv4mpt  32679  fsumiunle  32831  zarclsiin  33870  esumc  34052  esumrnmpt2  34069  esumgect  34091  esum2dlem  34093  esum2d  34094  esumiun  34095  ldsysgenld  34161  sigapildsys  34163  fiunelros  34175  omssubadd  34302  breprexplema  34645  bnj1491  35071  currysetlem  36946  currysetlem1  36948  ptrest  37626  aomclem8  43073  ss2iundf  43672  elunif  45021  rspcegf  45028  fiiuncl  45070  eliuniincex  45114  disjf1  45188  disjf1o  45196  iunmapsn  45222  fmptf  45245  infnsuprnmpt  45257  fmptff  45276  iuneqfzuzlem  45345  allbutfi  45404  supminfrnmpt  45456  supminfxrrnmpt  45482  monoordxr  45493  monoord2xr  45495  iooiinicc  45555  iooiinioc  45569  fsumiunss  45590  fprodcn  45615  climsuse  45623  climsubmpt  45675  climreclf  45679  fnlimcnv  45682  climeldmeqmpt  45683  climfveqmpt  45686  fnlimfvre  45689  fnlimabslt  45694  climfveqmpt3  45697  climbddf  45702  climeldmeqmpt3  45704  climinf2mpt  45729  climinfmpt  45730  limsupequzmptf  45746  lmbr3  45762  fprodcncf  45915  dvmptmulf  45952  dvnmptdivc  45953  dvnmul  45958  dvmptfprodlem  45959  dvnprodlem2  45962  stoweidlem59  46074  fourierdlem31  46153  sge00  46391  sge0pnffigt  46411  sge0lefi  46413  sge0resplit  46421  sge0lempt  46425  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0xadd  46450  sge0gtfsumgt  46458  iundjiun  46475  meadjiun  46481  meaiininclem  46501  omeiunltfirp  46534  hoidmvlelem1  46610  hoidmvlelem3  46612  hspdifhsp  46631  hoiqssbllem2  46638  hspmbllem2  46642  opnvonmbllem2  46648  hoimbl2  46680  vonhoire  46687  iinhoiicc  46689  iunhoiioo  46691  vonn0ioo2  46705  vonn0icc2  46707  incsmflem  46756  issmfle  46760  issmfgt  46771  decsmflem  46781  issmfge  46785  smflimlem2  46787  smflim  46792  smfresal  46803  smfpimbor1lem2  46814  smflim2  46821  smflimmpt  46825  smfsuplem1  46826  smfsupxr  46831  smfinflem  46832  smflimsuplem7  46841  smflimsuplem8  46842  smflimsup  46843  smflimsupmpt  46844  smfliminf  46846  smfliminfmpt  46847  nfdfat  47139