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

Syntax hints:  ⊤wtru 1535  Ⅎwnf 1778   ∈ wcel 2099  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779  df-cleq 2720  df-clel 2806  df-nfc 2881

This theorem is referenced by:  nfel1  2915  nfel2  2917  nfnel  3050  elabgf  3662  elrabf  3677  sbcel12  4405  rabxfrd  5412  ffnfvf  7125  nfixpw  8929  mptelixpg  8948  fsumsplit1  15718  ptcldmpt  23512  prdsdsf  24267  prdsxmet  24269  ssiun2sf  32344  iinabrex  32353  acunirnmpt2  32440  acunirnmpt2f  32441  aciunf1lem  32442  funcnv4mpt  32449  fsumiunle  32587  zarclsiin  33467  esumc  33665  esumrnmpt2  33682  esumgect  33704  esum2dlem  33706  esum2d  33707  esumiun  33708  ldsysgenld  33774  sigapildsys  33776  fiunelros  33788  omssubadd  33915  breprexplema  34257  bnj1491  34683  currysetlem  36419  currysetlem1  36421  ptrest  37087  aomclem8  42476  ss2iundf  43080  elunif  44369  rspcegf  44376  fiiuncl  44420  eliuniincex  44466  disjf1  44547  disjf1o  44555  iunmapsn  44581  fmptf  44605  infnsuprnmpt  44617  fmptff  44637  iuneqfzuzlem  44707  allbutfi  44766  supminfrnmpt  44818  supminfxrrnmpt  44844  monoordxr  44856  monoord2xr  44858  iooiinicc  44918  iooiinioc  44932  fsumiunss  44954  fprodcn  44979  climsuse  44987  climsubmpt  45039  climreclf  45043  fnlimcnv  45046  climeldmeqmpt  45047  climfveqmpt  45050  fnlimfvre  45053  fnlimabslt  45058  climfveqmpt3  45061  climbddf  45066  climeldmeqmpt3  45068  climinf2mpt  45093  climinfmpt  45094  limsupequzmptf  45110  lmbr3  45126  fprodcncf  45279  dvmptmulf  45316  dvnmptdivc  45317  dvnmul  45322  dvmptfprodlem  45323  dvmptfprod  45324  dvnprodlem1  45325  dvnprodlem2  45326  stoweidlem59  45438  fourierdlem31  45517  sge00  45755  sge0f1o  45761  sge0pnffigt  45775  sge0lefi  45777  sge0resplit  45785  sge0lempt  45789  sge0iunmptlemfi  45792  sge0iunmptlemre  45794  sge0iunmpt  45797  sge0xadd  45814  sge0gtfsumgt  45822  iundjiun  45839  meadjiun  45845  meaiininclem  45865  omeiunltfirp  45898  hoidmvlelem1  45974  hoidmvlelem3  45976  hspdifhsp  45995  hoiqssbllem2  46002  hspmbllem2  46006  opnvonmbllem2  46012  hoimbl2  46044  vonhoire  46051  iinhoiicc  46053  iunhoiioo  46055  vonn0ioo2  46069  vonn0icc2  46071  incsmflem  46120  issmfle  46124  issmfgt  46135  decsmflem  46145  issmfge  46149  smflimlem2  46151  smflim  46156  smfresal  46167  smfpimbor1lem2  46178  smflim2  46185  smflimmpt  46189  smfsuplem1  46190  smfsupxr  46195  smfinflem  46196  smfinfmpt  46198  smflimsuplem7  46205  smflimsuplem8  46206  smflimsup  46207  smflimsupmpt  46208  smfliminf  46210  smfliminfmpt  46211  nfdfat  46498