Theorem nfcsb1v 3873

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 2898	. 2 ⊢ Ⅎ𝑥𝐴
2	1	nfcsb1 3872	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Syntax hints:  Ⅎwnfc 2883  ⦋csb 3849

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-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-sbc 3741  df-csb 3850

This theorem is referenced by:  csbhypf  3877  csbiebt  3878  cbvrabcsfw  3890  cbvralcsf  3891  cbvreucsf  3893  cbvrabcsf  3894  rspc2vd  3897  sbcnestgfw  4373  sbcnestgf  4378  csbnest1g  4384  csbun  4393  csbin  4394  csbdif  4478  csbif  4537  disjors  5081  invdisjrab  5085  disjxiun  5095  disjxun  5096  sbcbr123  5152  eusvnf  5337  reusv2lem4  5346  reusv2  5348  moop2  5450  iunopeqop  5469  pofun  5550  opeliunxp  5691  opeliun2xp  5692  elrnmpt1  5909  resmptf  5998  csbima12  6038  csbcog  6255  fvmpt2f  6942  fvmpts  6944  fvmptdf  6947  fvmpt2i  6951  fvmptex  6955  fmptco  7074  fmptcof  7075  fmptcos  7076  elabrex  7188  elabrexg  7189  fliftfuns  7260  csbov123  7402  ovmpos  7506  fvmpopr2d  7520  ofmpteq  7645  mpomptsx  8008  dmmpossx  8010  fmpox  8011  el2mpocsbcl  8027  offval22  8030  ovmptss  8035  fmpoco  8037  dfmpo  8044  mpoxeldm  8153  mpocurryd  8211  mpocurryvald  8212  fvmpocurryd  8213  eqerlem  8670  qliftfuns  8741  mptelixpg  8873  boxcutc  8879  xpf1o  9067  iunfi  9243  wdom2d  9485  ixpiunwdom  9495  hsmexlem2  10337  ac6c4  10391  iundom2g  10450  seqof2  13983  rlimcld2  15501  nfsum1  15613  sumeq2ii  15616  summolem3  15637  summolem2a  15638  zsum  15641  fsum  15643  sumss2  15649  fsumcvg2  15650  fsumclf  15661  fsumzcl2  15662  fsumsplitf  15665  sumsnf  15666  sumsns  15673  fsummsnunz  15677  fsumsplitsnun  15678  fsum2dlem  15693  fsumcom2  15697  fsumshftm  15704  fsum0diag2  15706  fsum00  15721  fsumabs  15724  fsumrlim  15734  fsumo1  15735  o1fsum  15736  fsumiun  15744  infcvgaux1i  15780  nfcprod1  15831  prodeq2ii  15834  prodmolem3  15856  prodmolem2a  15857  zprod  15860  fprod  15864  fprodntriv  15865  prodss  15870  fprodser  15872  fprodcllemf  15881  prodsn  15885  prodsnf  15887  fprodm1s  15893  fprodp1s  15894  prodsns  15895  fprodabs  15897  fprodn0  15902  fprod2dlem  15903  fprodcom2  15907  fproddivf  15910  fprodsplitf  15911  fprodsplit1f  15913  fprodle  15919  fprodmodd  15920  fprodefsum  16018  sumeven  16314  sumodd  16315  pcmpt  16820  pcmptdvds  16822  natpropd  17903  fucpropd  17904  gsummpt1n0  19894  gsumcom2  19904  gsummptnn0fz  19915  dprd2d2  19975  psrass1lem  21888  mpfrcl  22040  coe1fzgsumdlem  22247  gsummoncoe1  22252  gsumply1eq  22253  evl1gsumdlem  22300  mdetralt2  22553  mdetunilem2  22557  madugsum  22587  fiuncmp  23348  ptcld  23557  ptcldmpt  23558  ptclsg  23559  elmptrab  23771  prdsdsf  24311  prdsxmet  24313  fsumcn  24817  fsum2cn  24818  ovolfiniun  25458  ovoliunlem3  25461  ovoliun  25462  ovoliun2  25463  ovoliunnul  25464  finiunmbl  25501  volfiniun  25504  iundisj  25505  iundisj2  25506  iunmbl  25510  iunmbl2  25514  itgss3  25772  itgfsum  25784  itgabs  25792  limciun  25851  dvmptfsum  25935  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  dvfsumlem4  25992  dvfsumrlim  25994  dvfsumrlim2  25995  dvfsum2  25997  itgsubstlem  26011  itgsubst  26012  rlimcnp2  26932  fsumdvdscom  27151  fsumdvdsmul  27161  fsumdvdsmulOLD  27163  fsumvma  27180  dchrisumlema  27455  dchrisumlem2  27457  dchrisumlem3  27458  iunxpssiun1  32643  disjorsf  32655  disjabrex  32657  disjabrexf  32658  iundisjf  32664  iundisj2f  32665  disjunsn  32669  suppss2f  32716  2ndresdju  32727  fmptdF  32734  fmptcof2  32735  acunirnmpt2f  32739  aciunf1lem  32740  funcnv4mpt  32747  f1od2  32798  iundisjfi  32876  iundisj2fi  32877  fsumiunle  32910  gsummpt2co  33131  gsummptp1  33140  gsumpart  33146  gsumvsca1  33308  gsumvsca2  33309  rmfsupp2  33320  esumpfinvalf  34233  esum2dlem  34249  esumiun  34251  fiunelros  34331  measiun  34375  voliune  34386  volfiniune  34387  sbcaltop  36175  weiunpo  36659  weiunso  36660  weiunfr  36661  weiunse  36662  bj-sbeqALT  37101  phpreu  37805  finixpnum  37806  ptrest  37820  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  poimirlem28  37849  mbfposadd  37868  itgabsnc  37890  ftc1cnnclem  37892  ftc2nc  37903  fsumshftd  39212  riotasv2s  39218  cdleme31sn  40640  cdleme31sn1  40641  cdleme31se2  40643  cdleme32fva  40697  cdleme42b  40738  hlhilset  42194  evl1gprodd  42371  idomnnzgmulnz  42387  deg1gprod  42394  fmpocos  42490  mzpsubst  42990  rabdiophlem2  43044  elnn0rabdioph  43045  dvdsrabdioph  43052  fphpd  43058  monotuz  43183  oddcomabszz  43186  wdom2d2  43277  aomclem6  43301  flcidc  43412  fsumcnf  45266  sumsnd  45271  fiiuncl  45310  eliin2f  45348  disjf1  45427  disjrnmpt2  45432  disjinfi  45436  fmptf  45483  fmptff  45513  iuneqfzuzlem  45579  supxrleubrnmptf  45695  fsummulc1f  45817  fsumnncl  45818  fsumf1of  45820  fsumiunss  45821  fsumreclf  45822  fsumlessf  45823  fprodexp  45840  fprodabs2  45841  mccllem  45843  fprodcnlem  45845  fprodcn  45846  climeldmeqmpt  45912  climeldmeqmpt3  45933  climinf2mpt  45958  climinfmpt  45959  limsupequzmptf  45975  fprodcncf  46144  dvmptmulf  46181  dvnmptdivc  46182  dvmptfprod  46189  iblsplitf  46214  fourierdlem86  46436  fourierdlem112  46462  sge0f1o  46626  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  sge0ltfirpmpt2  46670  sge0isummpt2  46676  sge0xaddlem2  46678  sge0xadd  46679  hoimbl2  46909  vonn0ioo2  46934  vonn0icc2  46936  csbafv12g  47383  csbaovg  47426  csbafv212g  47465  fsummsndifre  47618  fsumsplitsndif  47619  fsummmodsndifre  47620  fsummmodsnunz  47621  dmmpossx2  48583