Theorem nfel 2914

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-clel 2812  df-nfc 2886

This theorem is referenced by:  nfel1  2916  nfel2  2918  nfnel  3045  elabgf  3618  elrabf  3632  sbcel12  4352  rabxfrd  5354  ffnfvf  7066  nfixpw  8857  mptelixpg  8876  fsumsplit1  15698  ptcldmpt  23589  prdsdsf  24342  prdsxmet  24344  ssiun2sf  32644  iinabrex  32654  acunirnmpt2  32748  acunirnmpt2f  32749  aciunf1lem  32750  funcnv4mpt  32756  fsumiunle  32917  zarclsiin  34031  esumc  34211  esumrnmpt2  34228  esumgect  34250  esum2dlem  34252  esum2d  34253  esumiun  34254  ldsysgenld  34320  sigapildsys  34322  fiunelros  34334  omssubadd  34460  breprexplema  34790  bnj1491  35215  currysetlem  37268  currysetlem1  37270  ptrest  37954  aomclem8  43507  ss2iundf  44104  elunif  45465  rspcegf  45472  fiiuncl  45514  eliuniincex  45557  disjf1  45631  disjf1o  45639  iunmapsn  45664  fmptf  45686  infnsuprnmpt  45697  fmptff  45716  iuneqfzuzlem  45782  allbutfi  45840  supminfrnmpt  45891  supminfxrrnmpt  45917  monoordxr  45928  monoord2xr  45930  iooiinicc  45990  iooiinioc  46004  fsumiunss  46023  fprodcn  46048  climsuse  46056  climsubmpt  46106  climreclf  46110  fnlimcnv  46113  climeldmeqmpt  46114  climfveqmpt  46117  fnlimfvre  46120  fnlimabslt  46125  climfveqmpt3  46128  climbddf  46133  climeldmeqmpt3  46135  climinf2mpt  46160  climinfmpt  46161  limsupequzmptf  46177  lmbr3  46193  fprodcncf  46346  dvmptmulf  46383  dvnmptdivc  46384  dvnmul  46389  dvmptfprodlem  46390  dvnprodlem2  46393  stoweidlem59  46505  fourierdlem31  46584  sge00  46822  sge0pnffigt  46842  sge0lefi  46844  sge0resplit  46852  sge0lempt  46856  sge0iunmptlemfi  46859  sge0iunmptlemre  46861  sge0iunmpt  46864  sge0xadd  46881  sge0gtfsumgt  46889  iundjiun  46906  meadjiun  46912  meaiininclem  46932  omeiunltfirp  46965  hoidmvlelem1  47041  hoidmvlelem3  47043  hspdifhsp  47062  hoiqssbllem2  47069  hspmbllem2  47073  opnvonmbllem2  47079  hoimbl2  47111  vonhoire  47118  iinhoiicc  47120  iunhoiioo  47122  vonn0ioo2  47136  vonn0icc2  47138  incsmflem  47187  issmfle  47191  issmfgt  47202  decsmflem  47212  issmfge  47216  smflimlem2  47218  smflim  47223  smfresal  47234  smfpimbor1lem2  47245  smflim2  47252  smflimmpt  47256  smfsuplem1  47257  smfsupxr  47262  smfinflem  47263  smflimsuplem7  47272  smflimsuplem8  47273  smflimsup  47274  smflimsupmpt  47275  smfliminf  47277  smfliminfmpt  47278  nfdfat  47587