Theorem nfel1 2919

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

Syntax hints:  Ⅎwnf 1791   ∈ wcel 2121  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-nf 1792  df-cleq 2733  df-clel 2816  df-nfc 2890

This theorem is referenced by:  vtocl2gf  3516  vtocl3gf  3517  vtoclgaf  3520  vtocl2gaf  3523  vtocl3gaf  3524  nfop  4822  reusv2lem4  5332  reusv2  5334  rabxfrd  5348  pofun  5546  nfse  5594  fvmptf  6960  fmptcof  7075  fliftfuns  7261  riota2f  7340  ovmpos  7507  ov2gf  7508  elovmporab  7605  elovmporab1w  7606  elovmporab1  7607  ofmpteq  7646  fmpox  8011  offval22  8029  fvmpocurryd  8213  qliftfuns  8745  xpf1o  9071  iunfi  9247  wdom2d  9489  scottex  9804  dfac8clem  9949  ac6num  10397  pwfseqlem4a  10580  pwfseqlem4  10581  gruiin  10729  rlimcld2  15535  summolem3  15671  summolem2a  15672  zsum  15675  fsum  15677  sumss2  15683  fsumcvg2  15684  fsumclf  15695  fsumsplitf  15699  fsum2dlem  15727  fsumcom2  15731  fsumshftm  15738  fsum0diag2  15740  fsum00  15756  fsumabs  15759  fsumrlim  15769  fsumo1  15770  o1fsum  15771  fsumiun  15779  prodmolem3  15893  prodmolem2a  15894  zprod  15897  fprod  15901  prodss  15907  fprodser  15909  fprodm1s  15930  fprodp1s  15931  fprodabs  15934  fprodn0  15939  fprod2dlem  15940  fprodcom2  15944  fproddivf  15947  fprodsplitf  15948  fprodsplit1f  15950  fprodefsum  16055  pcmpt  16858  pcmptdvds  16860  gsumsnf  19922  gsumply1eq  22298  mdetralt2  22595  mdetunilem2  22599  fiuncmp  23390  elptr2  23560  ptcld  23599  ptcnplem  23607  ptcnp  23608  elmptrab  23813  utopsnneiplem  24233  prdsdsf  24353  prdsxmet  24355  fsumcn  24858  ovolfiniun  25489  ovoliunlem3  25492  ovoliun  25493  ovoliun2  25494  finiunmbl  25532  volfiniun  25535  iunmbl  25541  voliun  25542  itgfsum  25815  itgabs  25823  dvmptfsum  25963  dvfsumle  26009  dvfsumabs  26011  dvfsumlem1  26014  dvfsumlem3  26016  dvfsumlem4  26017  dvfsumrlim  26019  dvfsumrlim2  26020  dvfsum2  26022  itgsubst  26037  fsumdvdscom  27169  fsumvma  27197  dchrisumlema  27472  dchrisumlem2  27474  dchrisumlem3  27475  fsumiunle  32923  locfinreflem  34034  esumcl  34224  esum0  34243  esumcst  34257  esumfsup  34264  esum2d  34287  measiun  34412  voliune  34423  volfiniune  34424  iota5f  35965  weiunse  36709  phpreu  37984  poimirlem25  38025  poimirlem26  38026  poimirlem28  38028  itgabsnc  38069  fsumshftd  39457  riotasv2s  39463  cdlemefs32sn1aw  40919  mzpsubmpt  43205  mzpsubst  43210  eq0rabdioph  43238  eqrabdioph  43239  rabdiophlem2  43260  fphpd  43274  monotuz  43399  monotoddzz  43401  oddcomabszz  43402  flcidc  43628  binomcxplemdvbinom  44810  binomcxplemdvsum  44812  binomcxplemnotnn0  44813  modelaxreplem3  45437  rfcnnnub  45497  disjinfi  45651  supxrleubrnmptf  45906  caucvgbf  45944  cvgcaule  45946  fsummulc1f  46028  fsumnncl  46029  fsumf1of  46031  fsumreclf  46033  fsumlessf  46034  fsumsermpt  46036  fmul01  46037  fmuldfeqlem1  46039  fmuldfeq  46040  fmul01lt1lem1  46041  fmul01lt1lem2  46042  fprodexp  46051  fprodabs2  46052  fprodcnlem  46056  climmulf  46061  climsuse  46065  climrecf  46066  climaddf  46072  0ellimcdiv  46104  climsubmpt  46115  climfveqf  46135  climinf2mpt  46169  climinfmpt  46170  fprodcncf  46355  dvmptmulf  46392  dvmptfprod  46400  iblspltprt  46428  stoweidlem3  46458  stoweidlem19  46474  stoweidlem22  46477  stoweidlem42  46497  fourierdlem31  46593  fourierdlem86  46647  fourierdlem89  46650  fourierdlem91  46652  fourierdlem112  46673  sge0f1o  46837  sge0lempt  46865  sge0iunmpt  46873  sge0ltfirpmpt2  46881  sge0isummpt2  46887  sge0xaddlem2  46889  sge0xadd  46890  vonhoire  47127  salpreimagelt  47162  smflim  47232  smfresal  47243  smfinflem  47272  eu2ndop1stv  47600