Theorem nfel1 2922

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

Syntax hints:  Ⅎwnf 1787   ∈ wcel 2108  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-cleq 2730  df-clel 2817  df-nfc 2888

This theorem is referenced by:  vtocl2gf  3498  vtocl3gf  3499  vtoclgaf  3502  vtocl2gaf  3505  vtocl3gaf  3506  nfop  4817  reusv2lem4  5319  reusv2  5321  rabxfrd  5335  pofun  5512  nfse  5555  fvmptf  6878  fmptcof  6984  fliftfuns  7165  riota2f  7237  ovmpos  7399  ov2gf  7400  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  ofmpteq  7533  fmpox  7880  offval22  7899  fvmpocurryd  8058  qliftfuns  8551  xpf1o  8875  iunfi  9037  wdom2d  9269  scottex  9574  dfac8clem  9719  ac6num  10166  pwfseqlem4a  10348  pwfseqlem4  10349  gruiin  10497  rlimcld2  15215  summolem3  15354  summolem2a  15355  zsum  15358  fsum  15360  sumss2  15366  fsumcvg2  15367  fsumclf  15378  fsumsplitf  15382  fsum2dlem  15410  fsumcom2  15414  fsumshftm  15421  fsum0diag2  15423  fsum00  15438  fsumabs  15441  fsumrlim  15451  fsumo1  15452  o1fsum  15453  fsumiun  15461  prodmolem3  15571  prodmolem2a  15572  zprod  15575  fprod  15579  prodss  15585  fprodser  15587  fprodm1s  15608  fprodp1s  15609  fprodabs  15612  fprodn0  15617  fprod2dlem  15618  fprodcom2  15622  fproddivf  15625  fprodsplitf  15626  fprodsplit1f  15628  fprodefsum  15732  pcmpt  16521  pcmptdvds  16523  gsumsnf  19469  gsumply1eq  21386  mdetralt2  21666  mdetunilem2  21670  fiuncmp  22463  elptr2  22633  ptcld  22672  ptcnplem  22680  ptcnp  22681  elmptrab  22886  utopsnneiplem  23307  prdsdsf  23428  prdsxmet  23430  fsumcn  23939  ovolfiniun  24570  ovoliunlem3  24573  ovoliun  24574  ovoliun2  24575  finiunmbl  24613  volfiniun  24616  iunmbl  24622  voliun  24623  itgfsum  24896  itgabs  24904  dvmptfsum  25044  dvfsumle  25090  dvfsumabs  25092  dvfsumlem1  25095  dvfsumlem3  25097  dvfsumlem4  25098  dvfsumrlim  25100  dvfsumrlim2  25101  dvfsum2  25103  itgsubst  25118  fsumdvdscom  26239  fsumvma  26266  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  fsumiunle  31045  locfinreflem  31692  esumcl  31898  esum0  31917  esumcst  31931  esumfsup  31938  esum2d  31961  measiun  32086  voliune  32097  volfiniune  32098  iota5f  33571  phpreu  35688  poimirlem25  35729  poimirlem26  35730  poimirlem28  35732  itgabsnc  35773  fsumshftd  36893  riotasv2s  36899  cdlemefs32sn1aw  38355  mzpsubmpt  40481  mzpsubst  40486  eq0rabdioph  40514  eqrabdioph  40515  rabdiophlem2  40540  fphpd  40554  monotuz  40679  monotoddzz  40681  oddcomabszz  40682  flcidc  40915  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  rfcnnnub  42468  disjinfi  42620  supxrleubrnmptf  42881  fsummulc1f  43002  fsumnncl  43003  fsumf1of  43005  fsumreclf  43007  fsumlessf  43008  fsumsermpt  43010  fmul01  43011  fmuldfeqlem1  43013  fmuldfeq  43014  fmul01lt1lem1  43015  fmul01lt1lem2  43016  fprodexp  43025  fprodabs2  43026  fprodcnlem  43030  climmulf  43035  climsuse  43039  climrecf  43040  climaddf  43046  0ellimcdiv  43080  climsubmpt  43091  climfveqf  43111  climinf2mpt  43145  climinfmpt  43146  fprodcncf  43331  dvmptmulf  43368  iblspltprt  43404  stoweidlem3  43434  stoweidlem19  43450  stoweidlem22  43453  stoweidlem42  43473  fourierdlem31  43569  fourierdlem86  43623  fourierdlem89  43626  fourierdlem91  43628  fourierdlem112  43649  sge0f1o  43810  sge0lempt  43838  sge0iunmpt  43846  sge0ltfirpmpt2  43854  sge0isummpt2  43860  sge0xaddlem2  43862  sge0xadd  43863  vonhoire  44100  salpreimagelt  44132  smflim  44199  smfresal  44209  smfinflem  44237  eu2ndop1stv  44504