Theorem nfel 2940

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816   ∈ wcel 2147  Ⅎwnfc 2911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2755  df-clel 2839  df-nfc 2913

This theorem is used by:  nfel1  2942  nfel2  2944  nfnel  3073  elabgf  3631  elrabf  3645  sbcel12  4372  rabxfrd  5386  ffnfvf  7152  nfixpw  8982  mptelixpg  9001  fsumsplit1  15955  ptcldmpt  23988  prdsdsf  24741  prdsxmet  24743  ssiun2sf  33252  iinabrex  33261  aciunf1lem  33354  funcnv4mpt  33360  fsumiunle  33516  zarclsiin  34614  esumc  34794  esumrnmpt2  34811  esumgect  34833  esum2dlem  34835  esum2d  34836  esumiun  34837  ldsysgenld  34904  sigapildsys  34906  fiunelros  34918  breprexplema  35370  bnj1491  35798  currysetlem  38073  currysetlem1  38075  ptrest  38805  aomclem8  44329  ss2iundf  44920  elunif  46307  rspcegf  46314  fiiuncl  46356  eliuniincex  46397  disjf1  46471  disjf1o  46479  iunmapsn  46503  fmptf  46524  infnsuprnmpt  46535  fmptff  46554  iuneqfzuzlem  46619  allbutfi  46677  supminfrnmpt  46728  supminfxrrnmpt  46754  monoordxr  46765  monoord2xr  46767  iooiinicc  46827  iooiinioc  46841  fsumiunss  46860  fprodcn  46885  climsuse  46893  climsubmpt  46943  climreclf  46947  fnlimcnv  46950  climeldmeqmpt  46951  climfveqmpt  46954  fnlimfvre  46957  fnlimabslt  46962  climfveqmpt3  46965  climbddf  46970  climeldmeqmpt3  46972  climinf2mpt  46997  climinfmpt  46998  limsupequzmptf  47014  lmbr3  47030  fprodcncf  47183  dvmptmulf  47220  dvnmptdivc  47221  dvnmul  47226  dvmptfprodlem  47227  dvnprodlem2  47230  stoweidlem59  47342  fourierdlem31  47421  sge00  47659  sge0pnffigt  47679  sge0lefi  47681  sge0resplit  47689  sge0lempt  47693  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  sge0iunmpt  47701  sge0xadd  47718  sge0gtfsumgt  47726  iundjiun  47743  meadjiun  47749  meaiininclem  47769  omeiunltfirp  47802  hoidmvlelem1  47878  hoidmvlelem3  47880  hspdifhsp  47899  hoiqssbllem2  47906  hspmbllem2  47910  opnvonmbllem2  47916  hoimbl2  47948  vonhoire  47955  iinhoiicc  47957  iunhoiioo  47959  vonn0ioo2  47973  vonn0icc2  47975  incsmflem  48024  issmfle  48028  issmfgt  48039  decsmflem  48049  issmfge  48053  smflimlem2  48055  smflim  48060  smfresal  48071  smfpimbor1lem2  48082  smflim2  48089  smflimmpt  48093  smfsuplem1  48094  smfsupxr  48099  smfinflem  48100  smflimsuplem7  48109  smflimsuplem8  48110  smflimsup  48111  smflimsupmpt  48112  smfliminf  48114  smfliminfmpt  48115  nfdfat  48470