Theorem nfel1 2915

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2728  df-clel 2811  df-nfc 2885

This theorem is referenced by:  vtocl2gf  3527  vtocl3gf  3528  vtoclgaf  3531  vtocl2gaf  3534  vtocl2gafOLD  3535  vtocl3gaf  3536  vtocl3gafOLD  3537  nfop  4845  reusv2lem4  5346  reusv2  5348  rabxfrd  5362  pofun  5550  nfse  5598  fvmptf  6962  fmptcof  7075  fliftfuns  7260  riota2f  7339  ovmpos  7506  ov2gf  7507  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  ofmpteq  7645  fmpox  8011  offval22  8030  fvmpocurryd  8213  qliftfuns  8741  xpf1o  9067  iunfi  9243  wdom2d  9485  scottex  9797  dfac8clem  9942  ac6num  10389  pwfseqlem4a  10572  pwfseqlem4  10573  gruiin  10721  rlimcld2  15501  summolem3  15637  summolem2a  15638  zsum  15641  fsum  15643  sumss2  15649  fsumcvg2  15650  fsumclf  15661  fsumsplitf  15665  fsum2dlem  15693  fsumcom2  15697  fsumshftm  15704  fsum0diag2  15706  fsum00  15721  fsumabs  15724  fsumrlim  15734  fsumo1  15735  o1fsum  15736  fsumiun  15744  prodmolem3  15856  prodmolem2a  15857  zprod  15860  fprod  15864  prodss  15870  fprodser  15872  fprodm1s  15893  fprodp1s  15894  fprodabs  15897  fprodn0  15902  fprod2dlem  15903  fprodcom2  15907  fproddivf  15910  fprodsplitf  15911  fprodsplit1f  15913  fprodefsum  16018  pcmpt  16820  pcmptdvds  16822  gsumsnf  19882  gsumply1eq  22253  mdetralt2  22553  mdetunilem2  22557  fiuncmp  23348  elptr2  23518  ptcld  23557  ptcnplem  23565  ptcnp  23566  elmptrab  23771  utopsnneiplem  24191  prdsdsf  24311  prdsxmet  24313  fsumcn  24817  ovolfiniun  25458  ovoliunlem3  25461  ovoliun  25462  ovoliun2  25463  finiunmbl  25501  volfiniun  25504  iunmbl  25510  voliun  25511  itgfsum  25784  itgabs  25792  dvmptfsum  25935  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem3  25991  dvfsumlem4  25992  dvfsumrlim  25994  dvfsumrlim2  25995  dvfsum2  25997  itgsubst  26012  fsumdvdscom  27151  fsumvma  27180  dchrisumlema  27455  dchrisumlem2  27457  dchrisumlem3  27458  fsumiunle  32910  locfinreflem  33997  esumcl  34187  esum0  34206  esumcst  34220  esumfsup  34227  esum2d  34250  measiun  34375  voliune  34386  volfiniune  34387  iota5f  35918  weiunse  36662  phpreu  37805  poimirlem25  37846  poimirlem26  37847  poimirlem28  37849  itgabsnc  37890  fsumshftd  39212  riotasv2s  39218  cdlemefs32sn1aw  40674  mzpsubmpt  42985  mzpsubst  42990  eq0rabdioph  43018  eqrabdioph  43019  rabdiophlem2  43044  fphpd  43058  monotuz  43183  monotoddzz  43185  oddcomabszz  43186  flcidc  43412  binomcxplemdvbinom  44594  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  modelaxreplem3  45221  rfcnnnub  45281  disjinfi  45436  supxrleubrnmptf  45695  caucvgbf  45733  cvgcaule  45735  fsummulc1f  45817  fsumnncl  45818  fsumf1of  45820  fsumreclf  45822  fsumlessf  45823  fsumsermpt  45825  fmul01  45826  fmuldfeqlem1  45828  fmuldfeq  45829  fmul01lt1lem1  45830  fmul01lt1lem2  45831  fprodexp  45840  fprodabs2  45841  fprodcnlem  45845  climmulf  45850  climsuse  45854  climrecf  45855  climaddf  45861  0ellimcdiv  45893  climsubmpt  45904  climfveqf  45924  climinf2mpt  45958  climinfmpt  45959  fprodcncf  46144  dvmptmulf  46181  dvmptfprod  46189  iblspltprt  46217  stoweidlem3  46247  stoweidlem19  46263  stoweidlem22  46266  stoweidlem42  46286  fourierdlem31  46382  fourierdlem86  46436  fourierdlem89  46439  fourierdlem91  46441  fourierdlem112  46462  sge0f1o  46626  sge0lempt  46654  sge0iunmpt  46662  sge0ltfirpmpt2  46670  sge0isummpt2  46676  sge0xaddlem2  46678  sge0xadd  46679  vonhoire  46916  salpreimagelt  46951  smflim  47021  smfresal  47032  smfinflem  47061  eu2ndop1stv  47371