Theorem nfel1 2914

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 2897	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2912	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1782   ∈ wcel 2107  Ⅎwnfc 2882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-cleq 2726  df-clel 2808  df-nfc 2884

This theorem is referenced by:  vtocl2gf  3555  vtocl3gf  3556  vtoclgaf  3559  vtocl2gaf  3562  vtocl2gafOLD  3563  vtocl3gaf  3564  vtocl3gafOLD  3565  nfop  4869  reusv2lem4  5381  reusv2  5383  rabxfrd  5397  pofun  5590  nfse  5639  fvmptf  7017  fmptcof  7130  fliftfuns  7316  riota2f  7394  ovmpos  7563  ov2gf  7564  elovmporab  7661  elovmporab1w  7662  elovmporab1  7663  ofmpteq  7702  fmpox  8074  offval22  8095  fvmpocurryd  8278  qliftfuns  8826  xpf1o  9161  iunfi  9365  wdom2d  9602  scottex  9907  dfac8clem  10054  ac6num  10501  pwfseqlem4a  10683  pwfseqlem4  10684  gruiin  10832  rlimcld2  15597  summolem3  15733  summolem2a  15734  zsum  15737  fsum  15739  sumss2  15745  fsumcvg2  15746  fsumclf  15757  fsumsplitf  15761  fsum2dlem  15789  fsumcom2  15793  fsumshftm  15800  fsum0diag2  15802  fsum00  15817  fsumabs  15820  fsumrlim  15830  fsumo1  15831  o1fsum  15832  fsumiun  15840  prodmolem3  15952  prodmolem2a  15953  zprod  15956  fprod  15960  prodss  15966  fprodser  15968  fprodm1s  15989  fprodp1s  15990  fprodabs  15993  fprodn0  15998  fprod2dlem  15999  fprodcom2  16003  fproddivf  16006  fprodsplitf  16007  fprodsplit1f  16009  fprodefsum  16114  pcmpt  16913  pcmptdvds  16915  gsumsnf  19940  gsumply1eq  22262  mdetralt2  22564  mdetunilem2  22568  fiuncmp  23359  elptr2  23529  ptcld  23568  ptcnplem  23576  ptcnp  23577  elmptrab  23782  utopsnneiplem  24203  prdsdsf  24323  prdsxmet  24325  fsumcn  24831  ovolfiniun  25473  ovoliunlem3  25476  ovoliun  25477  ovoliun2  25478  finiunmbl  25516  volfiniun  25519  iunmbl  25525  voliun  25526  itgfsum  25799  itgabs  25807  dvmptfsum  25950  dvfsumle  25997  dvfsumleOLD  25998  dvfsumabs  26000  dvfsumlem1  26003  dvfsumlem3  26006  dvfsumlem4  26007  dvfsumrlim  26009  dvfsumrlim2  26010  dvfsum2  26012  itgsubst  26027  fsumdvdscom  27165  fsumvma  27194  dchrisumlema  27469  dchrisumlem2  27471  dchrisumlem3  27472  fsumiunle  32776  locfinreflem  33814  esumcl  34006  esum0  34025  esumcst  34039  esumfsup  34046  esum2d  34069  measiun  34194  voliune  34205  volfiniune  34206  iota5f  35699  weiunse  36444  phpreu  37586  poimirlem25  37627  poimirlem26  37628  poimirlem28  37630  itgabsnc  37671  fsumshftd  38928  riotasv2s  38934  cdlemefs32sn1aw  40391  mzpsubmpt  42732  mzpsubst  42737  eq0rabdioph  42765  eqrabdioph  42766  rabdiophlem2  42791  fphpd  42805  monotuz  42931  monotoddzz  42933  oddcomabszz  42934  flcidc  43160  binomcxplemdvbinom  44344  binomcxplemdvsum  44346  binomcxplemnotnn0  44347  modelaxreplem3  44969  rfcnnnub  45013  disjinfi  45169  supxrleubrnmptf  45434  caucvgbf  45472  cvgcaule  45474  fsummulc1f  45558  fsumnncl  45559  fsumf1of  45561  fsumreclf  45563  fsumlessf  45564  fsumsermpt  45566  fmul01  45567  fmuldfeqlem1  45569  fmuldfeq  45570  fmul01lt1lem1  45571  fmul01lt1lem2  45572  fprodexp  45581  fprodabs2  45582  fprodcnlem  45586  climmulf  45591  climsuse  45595  climrecf  45596  climaddf  45602  0ellimcdiv  45636  climsubmpt  45647  climfveqf  45667  climinf2mpt  45701  climinfmpt  45702  fprodcncf  45887  dvmptmulf  45924  dvmptfprod  45932  iblspltprt  45960  stoweidlem3  45990  stoweidlem19  46006  stoweidlem22  46009  stoweidlem42  46029  fourierdlem31  46125  fourierdlem86  46179  fourierdlem89  46182  fourierdlem91  46184  fourierdlem112  46205  sge0f1o  46369  sge0lempt  46397  sge0iunmpt  46405  sge0ltfirpmpt2  46413  sge0isummpt2  46419  sge0xaddlem2  46421  sge0xadd  46422  vonhoire  46659  salpreimagelt  46694  smflim  46764  smfresal  46775  smfinflem  46804  eu2ndop1stv  47110