Theorem nfel 2936

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

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 2752  df-clel 2835  df-nfc 2909

This theorem is used by:  nfel1  2938  nfel2  2940  nfnel  3069  elabgf  3628  elrabf  3642  sbcel12  4369  rabxfrd  5382  ffnfvf  7113  nfixpw  8923  mptelixpg  8942  fsumsplit1  15831  ptcldmpt  23840  prdsdsf  24593  prdsxmet  24595  ssiun2sf  33033  iinabrex  33042  acunirnmpt2  33133  acunirnmpt2f  33134  aciunf1lem  33135  funcnv4mpt  33141  fsumiunle  33299  zarclsiin  34381  esumc  34561  esumrnmpt2  34578  esumgect  34600  esum2dlem  34602  esum2d  34603  esumiun  34604  ldsysgenld  34671  sigapildsys  34673  fiunelros  34685  omssubadd  34811  breprexplema  35138  bnj1491  35566  currysetlem  37689  currysetlem1  37691  ptrest  38368  aomclem8  43902  ss2iundf  44499  elunif  45850  rspcegf  45857  fiiuncl  45899  eliuniincex  45941  disjf1  46015  disjf1o  46023  iunmapsn  46047  fmptf  46068  infnsuprnmpt  46079  fmptff  46098  iuneqfzuzlem  46164  allbutfi  46222  supminfrnmpt  46273  supminfxrrnmpt  46299  monoordxr  46310  monoord2xr  46312  iooiinicc  46372  iooiinioc  46386  fsumiunss  46405  fprodcn  46430  climsuse  46438  climsubmpt  46488  climreclf  46492  fnlimcnv  46495  climeldmeqmpt  46496  climfveqmpt  46499  fnlimfvre  46502  fnlimabslt  46507  climfveqmpt3  46510  climbddf  46515  climeldmeqmpt3  46517  climinf2mpt  46542  climinfmpt  46543  limsupequzmptf  46559  lmbr3  46575  fprodcncf  46728  dvmptmulf  46765  dvnmptdivc  46766  dvnmul  46771  dvmptfprodlem  46772  dvnprodlem2  46775  stoweidlem59  46887  fourierdlem31  46966  sge00  47204  sge0pnffigt  47224  sge0lefi  47226  sge0resplit  47234  sge0lempt  47238  sge0iunmptlemfi  47241  sge0iunmptlemre  47243  sge0iunmpt  47246  sge0xadd  47263  sge0gtfsumgt  47271  iundjiun  47288  meadjiun  47294  meaiininclem  47314  omeiunltfirp  47347  hoidmvlelem1  47423  hoidmvlelem3  47425  hspdifhsp  47444  hoiqssbllem2  47451  hspmbllem2  47455  opnvonmbllem2  47461  hoimbl2  47493  vonhoire  47500  iinhoiicc  47502  iunhoiioo  47504  vonn0ioo2  47518  vonn0icc2  47520  incsmflem  47569  issmfle  47573  issmfgt  47584  decsmflem  47594  issmfge  47598  smflimlem2  47600  smflim  47605  smfresal  47616  smfpimbor1lem2  47627  smflim2  47634  smflimmpt  47638  smfsuplem1  47639  smfsupxr  47644  smfinflem  47645  smflimsuplem7  47654  smflimsuplem8  47655  smflimsup  47656  smflimsupmpt  47657  smfliminf  47659  smfliminfmpt  47660  nfdfat  48015