Theorem nfel1 2939

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

Syntax hints:  Ⅎwnf 1811   ∈ wcel 2141  Ⅎwnfc 2908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-nf 1812  df-cleq 2753  df-clel 2836  df-nfc 2910

This theorem is referenced by:  vtocl2gf  3535  vtocl3gf  3536  vtoclgaf  3539  vtocl2gaf  3542  vtocl3gaf  3543  nfop  4853  reusv2lem4  5372  reusv2  5374  rabxfrd  5388  pofun  5587  nfse  5635  fvmptf  7011  fmptcof  7126  fliftfuns  7312  riota2f  7391  ovmpos  7558  ov2gf  7559  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  ofmpteq  7697  fmpox  8063  offval22  8082  fvmpocurryd  8266  qliftfuns  8801  xpf1o  9126  iunfi  9299  wdom2d  9541  scottex  9858  dfac8clem  10015  ac6num  10462  pwfseqlem4a  10645  pwfseqlem4  10646  gruiin  10794  rlimcld2  15628  summolem3  15764  summolem2a  15765  zsum  15768  fsum  15770  sumss2  15776  fsumcvg2  15777  fsumclf  15788  fsumsplitf  15792  fsum2dlem  15820  fsumcom2  15824  fsumshftm  15831  fsum0diag2  15833  fsum00  15849  fsumabs  15852  fsumrlim  15862  fsumo1  15863  o1fsum  15864  fsumiun  15872  prodmolem3  15986  prodmolem2a  15987  zprod  15990  fprod  15994  prodss  16000  fprodser  16002  fprodm1s  16023  fprodp1s  16024  fprodabs  16027  fprodn0  16032  fprod2dlem  16033  fprodcom2  16037  fproddivf  16040  fprodsplitf  16041  fprodsplit1f  16043  fprodefsum  16148  pcmpt  16951  pcmptdvds  16953  gsumsnf  20022  gsumply1eq  22448  mdetralt2  22745  mdetunilem2  22749  fiuncmp  23540  elptr2  23710  ptcld  23749  ptcnplem  23757  ptcnp  23758  elmptrab  23963  utopsnneiplem  24383  prdsdsf  24503  prdsxmet  24505  fsumcn  25008  ovolfiniun  25639  ovoliunlem3  25642  ovoliun  25643  ovoliun2  25644  finiunmbl  25682  volfiniun  25685  iunmbl  25691  voliun  25692  itgfsum  25965  itgabs  25973  dvmptfsum  26113  dvfsumle  26159  dvfsumabs  26161  dvfsumlem1  26164  dvfsumlem3  26166  dvfsumlem4  26167  dvfsumrlim  26169  dvfsumrlim2  26170  dvfsum2  26172  itgsubst  26187  fsumdvdscom  27325  fsumvma  27353  dchrisumlema  27628  dchrisumlem2  27630  dchrisumlem3  27631  fsumiunle  33139  locfinreflem  34196  esumcl  34386  esum0  34405  esumcst  34419  esumfsup  34426  esum2d  34449  measiun  34574  voliune  34585  volfiniune  34586  vonf1oonfo  35553  iota5f  36170  weiunse  36923  phpreu  38199  poimirlem25  38240  poimirlem26  38241  poimirlem28  38243  itgabsnc  38284  fsumshftd  39672  riotasv2s  39678  cdlemefs32sn1aw  41134  mzpsubmpt  43422  mzpsubst  43427  eq0rabdioph  43455  eqrabdioph  43456  rabdiophlem2  43477  fphpd  43491  monotuz  43616  monotoddzz  43618  oddcomabszz  43619  flcidc  43845  binomcxplemdvbinom  45011  binomcxplemdvsum  45013  binomcxplemnotnn0  45014  modelaxreplem3  45637  rfcnnnub  45704  disjinfi  45858  supxrleubrnmptf  46113  caucvgbf  46151  cvgcaule  46153  fsummulc1f  46235  fsumnncl  46236  fsumf1of  46238  fsumreclf  46240  fsumlessf  46241  fsumsermpt  46243  fmul01  46244  fmuldfeqlem1  46246  fmuldfeq  46247  fmul01lt1lem1  46248  fmul01lt1lem2  46249  fprodexp  46258  fprodabs2  46259  fprodcnlem  46263  climmulf  46268  climsuse  46272  climrecf  46273  climaddf  46279  0ellimcdiv  46311  climsubmpt  46322  climfveqf  46342  climinf2mpt  46376  climinfmpt  46377  fprodcncf  46562  dvmptmulf  46599  dvmptfprod  46607  iblspltprt  46635  stoweidlem3  46665  stoweidlem19  46681  stoweidlem22  46684  stoweidlem42  46704  fourierdlem31  46800  fourierdlem86  46854  fourierdlem89  46857  fourierdlem91  46859  fourierdlem112  46880  sge0f1o  47044  sge0lempt  47072  sge0iunmpt  47080  sge0ltfirpmpt2  47088  sge0isummpt2  47094  sge0xaddlem2  47096  sge0xadd  47097  vonhoire  47334  salpreimagelt  47369  smflim  47439  smfresal  47450  smfinflem  47479  eu2ndop1stv  47807