Theorem nfel 2941

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

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

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

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 2757  df-clel 2840  df-nfc 2914

This theorem is used by:  nfel1  2943  nfel2  2945  nfnel  3074  elabgf  3635  elrabf  3649  sbcel12  4376  rabxfrd  5390  ffnfvf  7119  nfixpw  8916  mptelixpg  8935  fsumsplit1  15814  ptcldmpt  23800  prdsdsf  24553  prdsxmet  24555  ssiun2sf  32933  iinabrex  32943  acunirnmpt2  33034  acunirnmpt2f  33035  aciunf1lem  33036  funcnv4mpt  33042  fsumiunle  33202  zarclsiin  34284  esumc  34464  esumrnmpt2  34481  esumgect  34503  esum2dlem  34505  esum2d  34506  esumiun  34507  ldsysgenld  34574  sigapildsys  34576  fiunelros  34588  omssubadd  34714  breprexplema  35041  bnj1491  35469  currysetlem  37614  currysetlem1  37616  ptrest  38303  aomclem8  43821  ss2iundf  44418  elunif  45769  rspcegf  45776  fiiuncl  45818  eliuniincex  45860  disjf1  45934  disjf1o  45942  iunmapsn  45966  fmptf  45987  infnsuprnmpt  45998  fmptff  46017  iuneqfzuzlem  46083  allbutfi  46141  supminfrnmpt  46192  supminfxrrnmpt  46218  monoordxr  46229  monoord2xr  46231  iooiinicc  46291  iooiinioc  46305  fsumiunss  46324  fprodcn  46349  climsuse  46357  climsubmpt  46407  climreclf  46411  fnlimcnv  46414  climeldmeqmpt  46415  climfveqmpt  46418  fnlimfvre  46421  fnlimabslt  46426  climfveqmpt3  46429  climbddf  46434  climeldmeqmpt3  46436  climinf2mpt  46461  climinfmpt  46462  limsupequzmptf  46478  lmbr3  46494  fprodcncf  46647  dvmptmulf  46684  dvnmptdivc  46685  dvnmul  46690  dvmptfprodlem  46691  dvnprodlem2  46694  stoweidlem59  46806  fourierdlem31  46885  sge00  47123  sge0pnffigt  47143  sge0lefi  47145  sge0resplit  47153  sge0lempt  47157  sge0iunmptlemfi  47160  sge0iunmptlemre  47162  sge0iunmpt  47165  sge0xadd  47182  sge0gtfsumgt  47190  iundjiun  47207  meadjiun  47213  meaiininclem  47233  omeiunltfirp  47266  hoidmvlelem1  47342  hoidmvlelem3  47344  hspdifhsp  47363  hoiqssbllem2  47370  hspmbllem2  47374  opnvonmbllem2  47380  hoimbl2  47412  vonhoire  47419  iinhoiicc  47421  iunhoiioo  47423  vonn0ioo2  47437  vonn0icc2  47439  incsmflem  47488  issmfle  47492  issmfgt  47503  decsmflem  47513  issmfge  47517  smflimlem2  47519  smflim  47524  smfresal  47535  smfpimbor1lem2  47546  smflim2  47553  smflimmpt  47557  smfsuplem1  47558  smfsupxr  47563  smfinflem  47564  smflimsuplem7  47573  smflimsuplem8  47574  smflimsup  47575  smflimsupmpt  47576  smfliminf  47578  smfliminfmpt  47579  nfdfat  47897