Theorem nfel 2937

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

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

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 2733

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 2753  df-clel 2836  df-nfc 2910

This theorem is used by:  nfel1  2939  nfel2  2941  nfnel  3070  elabgf  3628  elrabf  3642  sbcel12  4369  rabxfrd  5379  ffnfvf  7118  nfixpw  8937  mptelixpg  8956  fsumsplit1  15904  ptcldmpt  23926  prdsdsf  24679  prdsxmet  24681  ssiun2sf  33147  iinabrex  33156  acunirnmpt2  33247  acunirnmpt2f  33248  aciunf1lem  33249  funcnv4mpt  33255  fsumiunle  33413  zarclsiin  34496  esumc  34676  esumrnmpt2  34693  esumgect  34715  esum2dlem  34717  esum2d  34718  esumiun  34719  ldsysgenld  34786  sigapildsys  34788  fiunelros  34800  omssubadd  34925  breprexplema  35252  bnj1491  35680  currysetlem  37838  currysetlem1  37840  ptrest  38517  aomclem8  44047  ss2iundf  44644  elunif  46002  rspcegf  46009  fiiuncl  46051  eliuniincex  46093  disjf1  46167  disjf1o  46175  iunmapsn  46199  fmptf  46220  infnsuprnmpt  46231  fmptff  46250  iuneqfzuzlem  46315  allbutfi  46373  supminfrnmpt  46424  supminfxrrnmpt  46450  monoordxr  46461  monoord2xr  46463  iooiinicc  46523  iooiinioc  46537  fsumiunss  46556  fprodcn  46581  climsuse  46589  climsubmpt  46639  climreclf  46643  fnlimcnv  46646  climeldmeqmpt  46647  climfveqmpt  46650  fnlimfvre  46653  fnlimabslt  46658  climfveqmpt3  46661  climbddf  46666  climeldmeqmpt3  46668  climinf2mpt  46693  climinfmpt  46694  limsupequzmptf  46710  lmbr3  46726  fprodcncf  46879  dvmptmulf  46916  dvnmptdivc  46917  dvnmul  46922  dvmptfprodlem  46923  dvnprodlem2  46926  stoweidlem59  47038  fourierdlem31  47117  sge00  47355  sge0pnffigt  47375  sge0lefi  47377  sge0resplit  47385  sge0lempt  47389  sge0iunmptlemfi  47392  sge0iunmptlemre  47394  sge0iunmpt  47397  sge0xadd  47414  sge0gtfsumgt  47422  iundjiun  47439  meadjiun  47445  meaiininclem  47465  omeiunltfirp  47498  hoidmvlelem1  47574  hoidmvlelem3  47576  hspdifhsp  47595  hoiqssbllem2  47602  hspmbllem2  47606  opnvonmbllem2  47612  hoimbl2  47644  vonhoire  47651  iinhoiicc  47653  iunhoiioo  47655  vonn0ioo2  47669  vonn0icc2  47671  incsmflem  47720  issmfle  47724  issmfgt  47735  decsmflem  47745  issmfge  47749  smflimlem2  47751  smflim  47756  smfresal  47767  smfpimbor1lem2  47778  smflim2  47785  smflimmpt  47789  smfsuplem1  47790  smfsupxr  47795  smfinflem  47796  smflimsuplem7  47805  smflimsuplem8  47806  smflimsup  47807  smflimsupmpt  47808  smfliminf  47810  smfliminfmpt  47811  nfdfat  48166