Theorem nfel1 2942

Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq1.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfel1	⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Distinct variable group:   𝑥,𝐵

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfel1

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2926	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2940	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1805   ∈ wcel 2144  Ⅎwnfc 2911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-ex 1802  df-nf 1806  df-cleq 2756  df-clel 2839  df-nfc 2913

This theorem is referenced by:  vtocl2gf  3538  vtocl3gf  3539  vtoclgaf  3542  vtocl2gaf  3545  vtocl3gaf  3546  nfop  4849  reusv2lem4  5360  reusv2  5362  rabxfrd  5376  pofun  5575  nfse  5623  fvmptf  6999  fmptcof  7114  fliftfuns  7300  riota2f  7379  ovmpos  7546  ov2gf  7547  elovmporab  7644  elovmporab1w  7645  elovmporab1  7646  ofmpteq  7685  fmpox  8050  offval22  8069  fvmpocurryd  8253  qliftfuns  8788  xpf1o  9113  iunfi  9288  wdom2d  9530  scottex  9845  dfac8clem  9990  ac6num  10438  pwfseqlem4a  10621  pwfseqlem4  10622  gruiin  10770  rlimcld2  15607  summolem3  15743  summolem2a  15744  zsum  15747  fsum  15749  sumss2  15755  fsumcvg2  15756  fsumclf  15767  fsumsplitf  15771  fsum2dlem  15799  fsumcom2  15803  fsumshftm  15810  fsum0diag2  15812  fsum00  15828  fsumabs  15831  fsumrlim  15841  fsumo1  15842  o1fsum  15843  fsumiun  15851  prodmolem3  15965  prodmolem2a  15966  zprod  15969  fprod  15973  prodss  15979  fprodser  15981  fprodm1s  16002  fprodp1s  16003  fprodabs  16006  fprodn0  16011  fprod2dlem  16012  fprodcom2  16016  fproddivf  16019  fprodsplitf  16020  fprodsplit1f  16022  fprodefsum  16127  pcmpt  16930  pcmptdvds  16932  gsumsnf  19995  gsumply1eq  22374  mdetralt2  22671  mdetunilem2  22675  fiuncmp  23466  elptr2  23636  ptcld  23675  ptcnplem  23683  ptcnp  23684  elmptrab  23889  utopsnneiplem  24309  prdsdsf  24429  prdsxmet  24431  fsumcn  24934  ovolfiniun  25565  ovoliunlem3  25568  ovoliun  25569  ovoliun2  25570  finiunmbl  25608  volfiniun  25611  iunmbl  25617  voliun  25618  itgfsum  25891  itgabs  25899  dvmptfsum  26039  dvfsumle  26085  dvfsumabs  26087  dvfsumlem1  26090  dvfsumlem3  26092  dvfsumlem4  26093  dvfsumrlim  26095  dvfsumrlim2  26096  dvfsum2  26098  itgsubst  26113  fsumdvdscom  27251  fsumvma  27279  dchrisumlema  27554  dchrisumlem2  27556  dchrisumlem3  27557  fsumiunle  33033  locfinreflem  34139  esumcl  34329  esum0  34348  esumcst  34362  esumfsup  34369  esum2d  34392  measiun  34517  voliune  34528  volfiniune  34529  vonf1oonfo  35462  iota5f  36079  weiunse  36833  phpreu  38108  poimirlem25  38149  poimirlem26  38150  poimirlem28  38152  itgabsnc  38193  fsumshftd  39581  riotasv2s  39587  cdlemefs32sn1aw  41043  mzpsubmpt  43329  mzpsubst  43334  eq0rabdioph  43362  eqrabdioph  43363  rabdiophlem2  43384  fphpd  43398  monotuz  43523  monotoddzz  43525  oddcomabszz  43526  flcidc  43752  binomcxplemdvbinom  44934  binomcxplemdvsum  44936  binomcxplemnotnn0  44937  modelaxreplem3  45561  rfcnnnub  45621  disjinfi  45775  supxrleubrnmptf  46030  caucvgbf  46068  cvgcaule  46070  fsummulc1f  46152  fsumnncl  46153  fsumf1of  46155  fsumreclf  46157  fsumlessf  46158  fsumsermpt  46160  fmul01  46161  fmuldfeqlem1  46163  fmuldfeq  46164  fmul01lt1lem1  46165  fmul01lt1lem2  46166  fprodexp  46175  fprodabs2  46176  fprodcnlem  46180  climmulf  46185  climsuse  46189  climrecf  46190  climaddf  46196  0ellimcdiv  46228  climsubmpt  46239  climfveqf  46259  climinf2mpt  46293  climinfmpt  46294  fprodcncf  46479  dvmptmulf  46516  dvmptfprod  46524  iblspltprt  46552  stoweidlem3  46582  stoweidlem19  46598  stoweidlem22  46601  stoweidlem42  46621  fourierdlem31  46717  fourierdlem86  46771  fourierdlem89  46774  fourierdlem91  46776  fourierdlem112  46797  sge0f1o  46961  sge0lempt  46989  sge0iunmpt  46997  sge0ltfirpmpt2  47005  sge0isummpt2  47011  sge0xaddlem2  47013  sge0xadd  47014  vonhoire  47251  salpreimagelt  47286  smflim  47356  smfresal  47367  smfinflem  47396  eu2ndop1stv  47724