Theorem nfel 2913

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2727  df-clel 2809  df-nfc 2885

This theorem is referenced by:  nfel1  2915  nfel2  2917  nfnel  3044  elabgf  3653  elrabf  3667  sbcel12  4386  rabxfrd  5387  ffnfvf  7110  nfixpw  8930  mptelixpg  8949  fsumsplit1  15761  ptcldmpt  23552  prdsdsf  24306  prdsxmet  24308  ssiun2sf  32540  iinabrex  32550  acunirnmpt2  32638  acunirnmpt2f  32639  aciunf1lem  32640  funcnv4mpt  32647  fsumiunle  32808  zarclsiin  33902  esumc  34082  esumrnmpt2  34099  esumgect  34121  esum2dlem  34123  esum2d  34124  esumiun  34125  ldsysgenld  34191  sigapildsys  34193  fiunelros  34205  omssubadd  34332  breprexplema  34662  bnj1491  35088  currysetlem  36963  currysetlem1  36965  ptrest  37643  aomclem8  43085  ss2iundf  43683  elunif  45040  rspcegf  45047  fiiuncl  45089  eliuniincex  45133  disjf1  45207  disjf1o  45215  iunmapsn  45241  fmptf  45263  infnsuprnmpt  45274  fmptff  45293  iuneqfzuzlem  45361  allbutfi  45420  supminfrnmpt  45472  supminfxrrnmpt  45498  monoordxr  45509  monoord2xr  45511  iooiinicc  45571  iooiinioc  45585  fsumiunss  45604  fprodcn  45629  climsuse  45637  climsubmpt  45689  climreclf  45693  fnlimcnv  45696  climeldmeqmpt  45697  climfveqmpt  45700  fnlimfvre  45703  fnlimabslt  45708  climfveqmpt3  45711  climbddf  45716  climeldmeqmpt3  45718  climinf2mpt  45743  climinfmpt  45744  limsupequzmptf  45760  lmbr3  45776  fprodcncf  45929  dvmptmulf  45966  dvnmptdivc  45967  dvnmul  45972  dvmptfprodlem  45973  dvnprodlem2  45976  stoweidlem59  46088  fourierdlem31  46167  sge00  46405  sge0pnffigt  46425  sge0lefi  46427  sge0resplit  46435  sge0lempt  46439  sge0iunmptlemfi  46442  sge0iunmptlemre  46444  sge0iunmpt  46447  sge0xadd  46464  sge0gtfsumgt  46472  iundjiun  46489  meadjiun  46495  meaiininclem  46515  omeiunltfirp  46548  hoidmvlelem1  46624  hoidmvlelem3  46626  hspdifhsp  46645  hoiqssbllem2  46652  hspmbllem2  46656  opnvonmbllem2  46662  hoimbl2  46694  vonhoire  46701  iinhoiicc  46703  iunhoiioo  46705  vonn0ioo2  46719  vonn0icc2  46721  incsmflem  46770  issmfle  46774  issmfgt  46785  decsmflem  46795  issmfge  46799  smflimlem2  46801  smflim  46806  smfresal  46817  smfpimbor1lem2  46828  smflim2  46835  smflimmpt  46839  smfsuplem1  46840  smfsupxr  46845  smfinflem  46846  smflimsuplem7  46855  smflimsuplem8  46856  smflimsup  46857  smflimsupmpt  46858  smfliminf  46860  smfliminfmpt  46861  nfdfat  47156