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 1548	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2728  df-clel 2811  df-nfc 2885

This theorem is referenced by:  nfel1  2915  nfel2  2917  nfnel  3044  elabgf  3629  elrabf  3643  sbcel12  4363  rabxfrd  5362  ffnfvf  7065  nfixpw  8854  mptelixpg  8873  fsumsplit1  15668  ptcldmpt  23558  prdsdsf  24311  prdsxmet  24313  ssiun2sf  32634  iinabrex  32644  acunirnmpt2  32738  acunirnmpt2f  32739  aciunf1lem  32740  funcnv4mpt  32747  fsumiunle  32910  zarclsiin  34028  esumc  34208  esumrnmpt2  34225  esumgect  34247  esum2dlem  34249  esum2d  34250  esumiun  34251  ldsysgenld  34317  sigapildsys  34319  fiunelros  34331  omssubadd  34457  breprexplema  34787  bnj1491  35213  currysetlem  37146  currysetlem1  37148  ptrest  37820  aomclem8  43303  ss2iundf  43900  elunif  45261  rspcegf  45268  fiiuncl  45310  eliuniincex  45353  disjf1  45427  disjf1o  45435  iunmapsn  45461  fmptf  45483  infnsuprnmpt  45494  fmptff  45513  iuneqfzuzlem  45579  allbutfi  45637  supminfrnmpt  45689  supminfxrrnmpt  45715  monoordxr  45726  monoord2xr  45728  iooiinicc  45788  iooiinioc  45802  fsumiunss  45821  fprodcn  45846  climsuse  45854  climsubmpt  45904  climreclf  45908  fnlimcnv  45911  climeldmeqmpt  45912  climfveqmpt  45915  fnlimfvre  45918  fnlimabslt  45923  climfveqmpt3  45926  climbddf  45931  climeldmeqmpt3  45933  climinf2mpt  45958  climinfmpt  45959  limsupequzmptf  45975  lmbr3  45991  fprodcncf  46144  dvmptmulf  46181  dvnmptdivc  46182  dvnmul  46187  dvmptfprodlem  46188  dvnprodlem2  46191  stoweidlem59  46303  fourierdlem31  46382  sge00  46620  sge0pnffigt  46640  sge0lefi  46642  sge0resplit  46650  sge0lempt  46654  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  sge0xadd  46679  sge0gtfsumgt  46687  iundjiun  46704  meadjiun  46710  meaiininclem  46730  omeiunltfirp  46763  hoidmvlelem1  46839  hoidmvlelem3  46841  hspdifhsp  46860  hoiqssbllem2  46867  hspmbllem2  46871  opnvonmbllem2  46877  hoimbl2  46909  vonhoire  46916  iinhoiicc  46918  iunhoiioo  46920  vonn0ioo2  46934  vonn0icc2  46936  incsmflem  46985  issmfle  46989  issmfgt  47000  decsmflem  47010  issmfge  47014  smflimlem2  47016  smflim  47021  smfresal  47032  smfpimbor1lem2  47043  smflim2  47050  smflimmpt  47054  smfsuplem1  47055  smfsupxr  47060  smfinflem  47061  smflimsuplem7  47070  smflimsuplem8  47071  smflimsup  47072  smflimsupmpt  47073  smfliminf  47075  smfliminfmpt  47076  nfdfat  47373