Theorem nfcsb1v 3874

Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)

Assertion

Ref	Expression
nfcsb1v	⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfcsb1v

Step	Hyp	Ref	Expression
1		nfcv 2923	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfcsb1 3873	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Syntax hints:  Ⅎwnfc 2908  ⦋csb 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  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 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-sbc 3743  df-csb 3851

This theorem is referenced by:  csbhypf  3878  csbiebt  3879  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  rspc2vd  3898  sbcnestgfw  4372  sbcnestgf  4377  csbnest1g  4383  csbun  4392  csbin  4393  csbdif  4476  csbif  4535  disjors  5080  invdisjrab  5084  disjxiun  5094  disjxun  5095  sbcbr123  5151  eusvnf  5346  reusv2lem4  5355  reusv2  5357  moop2  5468  iunopeqop  5487  iunopeqopOLD  5488  pofun  5569  opeliunxp  5710  opeliun2xp  5711  elrnmpt1  5932  resmptf  6023  csbima12  6063  csbcog  6278  fvmpt2f  6970  fvmpts  6973  fvmptdf  6976  fvmpt2i  6980  fvmptex  6984  fmptco  7105  fmptcof  7106  fmptcos  7107  elabrex  7220  elabrexg  7221  fliftfuns  7292  csbov123  7434  ovmpos  7538  fvmpopr2d  7552  ofmpteq  7677  mpomptsx  8039  dmmpossx  8041  fmpox  8042  el2mpocsbcl  8057  offval22  8060  ovmptss  8065  fmpoco  8067  dfmpo  8074  mpoxeldm  8184  mpocurryd  8242  mpocurryvald  8243  fvmpocurryd  8244  eqerlem  8707  qliftfuns  8779  mptelixpg  8910  boxcutc  8916  xpf1o  9104  iunfi  9279  wdom2d  9521  ixpiunwdom  9531  hsmexlem2  10377  ac6c4  10431  iundom2g  10490  seqof2  14066  rlimcld2  15595  nfsum1  15707  sumeq2ii  15710  summolem3  15731  summolem2a  15732  zsum  15735  fsum  15737  sumss2  15743  fsumcvg2  15744  fsumclf  15755  fsumzcl2  15756  fsumsplitf  15759  sumsnf  15760  sumsns  15767  fsummsnunz  15771  fsumsplitsnun  15772  fsum2dlem  15787  fsumcom2  15791  fsumshftm  15798  fsum0diag2  15800  fsum00  15816  fsumabs  15819  fsumrlim  15829  fsumo1  15830  o1fsum  15831  fsumiun  15839  infcvgaux1i  15877  nfcprod1  15928  prodeq2ii  15931  prodmolem3  15953  prodmolem2a  15954  zprod  15957  fprod  15961  fprodntriv  15962  prodss  15967  fprodser  15969  fprodcllemf  15978  prodsn  15982  prodsnf  15984  fprodm1s  15990  fprodp1s  15991  prodsns  15992  fprodabs  15994  fprodn0  15999  fprod2dlem  16000  fprodcom2  16004  fproddivf  16007  fprodsplitf  16008  fprodsplit1f  16010  fprodle  16016  fprodmodd  16017  fprodefsum  16115  sumeven  16411  sumodd  16412  pcmpt  16918  pcmptdvds  16920  natpropd  18002  fucpropd  18003  gsummpt1n0  19995  gsumcom2  20005  gsummptnn0fz  20016  dprd2d2  20076  psrass1lem  21972  mpfrcl  22125  coe1fzgsumdlem  22353  gsummoncoe1  22358  gsumply1eq  22359  evl1gsumdlem  22406  mdetralt2  22656  mdetunilem2  22660  madugsum  22690  fiuncmp  23451  ptcld  23660  ptcldmpt  23661  ptclsg  23662  elmptrab  23874  prdsdsf  24414  prdsxmet  24416  fsumcn  24919  fsum2cn  24920  ovolfiniun  25550  ovoliunlem3  25553  ovoliun  25554  ovoliun2  25555  ovoliunnul  25556  finiunmbl  25593  volfiniun  25596  iundisj  25597  iundisj2  25598  iunmbl  25602  iunmbl2  25606  itgss3  25864  itgfsum  25876  itgabs  25884  limciun  25943  dvmptfsum  26024  dvfsumle  26070  dvfsumabs  26072  dvfsumlem1  26075  dvfsumlem2  26076  dvfsumlem3  26077  dvfsumlem4  26078  dvfsumrlim  26080  dvfsumrlim2  26081  dvfsum2  26083  itgsubstlem  26097  itgsubst  26098  rlimcnp2  27018  fsumdvdscom  27236  fsumdvdsmul  27246  fsumvma  27264  dchrisumlema  27539  dchrisumlem2  27541  dchrisumlem3  27542  iunxpssiun1  32727  disjorsf  32739  disjabrex  32741  disjabrexf  32742  iundisjf  32748  iundisj2f  32749  disjunsn  32753  suppss2f  32800  2ndresdju  32811  fmptdF  32818  fmptcof2  32819  acunirnmpt2f  32823  aciunf1lem  32824  funcnv4mpt  32830  f1od2  32881  iundisjfi  32958  iundisj2fi  32959  fsumiunle  32991  gsummpt2co  33188  gsummptp1  33197  gsumpart  33203  gsumvsca1  33366  gsumvsca2  33367  rmfsupp2  33378  esumpfinvalf  34333  esum2dlem  34349  esumiun  34351  fiunelros  34431  measiun  34475  voliune  34486  volfiniune  34487  sbcaltop  36291  weiunpo  36785  weiunso  36786  weiunfr  36787  weiunse  36788  csbttc  36829  bj-sbeqALT  37345  phpreu  38063  finixpnum  38064  ptrest  38078  poimirlem23  38102  poimirlem24  38103  poimirlem25  38104  poimirlem26  38105  poimirlem27  38106  poimirlem28  38107  mbfposadd  38126  itgabsnc  38148  ftc1cnnclem  38150  ftc2nc  38161  fsumshftd  39536  riotasv2s  39542  cdleme31sn  40964  cdleme31sn1  40965  cdleme31se2  40967  cdleme32fva  41021  cdleme42b  41062  hlhilset  42518  evl1gprodd  42694  idomnnzgmulnz  42710  deg1gprod  42717  fmpocos  42812  mzpsubst  43289  rabdiophlem2  43339  elnn0rabdioph  43340  dvdsrabdioph  43347  fphpd  43353  monotuz  43478  oddcomabszz  43481  wdom2d2  43572  aomclem6  43596  flcidc  43707  fsumcnf  45561  sumsnd  45566  fiiuncl  45605  eliin2f  45642  disjf1  45721  disjrnmpt2  45726  disjinfi  45730  fmptf  45774  fmptff  45804  iuneqfzuzlem  45870  supxrleubrnmptf  45985  fsummulc1f  46107  fsumnncl  46108  fsumf1of  46110  fsumiunss  46111  fsumreclf  46112  fsumlessf  46113  fprodexp  46130  fprodabs2  46131  mccllem  46133  fprodcnlem  46135  fprodcn  46136  climeldmeqmpt  46202  climeldmeqmpt3  46223  climinf2mpt  46248  climinfmpt  46249  limsupequzmptf  46265  fprodcncf  46434  dvmptmulf  46471  dvnmptdivc  46472  dvmptfprod  46479  iblsplitf  46504  fourierdlem86  46726  fourierdlem112  46752  sge0f1o  46916  sge0iunmptlemfi  46947  sge0iunmptlemre  46949  sge0iunmpt  46952  sge0ltfirpmpt2  46960  sge0isummpt2  46966  sge0xaddlem2  46968  sge0xadd  46969  hoimbl2  47199  vonn0ioo2  47224  vonn0icc2  47226  csbafv12g  47691  csbaovg  47734  csbafv212g  47773  fsummsndifre  47934  fsumsplitsndif  47935  fsummmodsndifre  47936  fsummmodsnunz  47937  dmmpossx2  48919