Theorem nfcsb1v 3889

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

Syntax hints:  Ⅎwnfc 2877  ⦋csb 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-sbc 3757  df-csb 3866

This theorem is referenced by:  csbhypf  3893  csbiebt  3894  cbvrabcsfw  3906  cbvralcsf  3907  cbvreucsf  3909  cbvrabcsf  3910  rspc2vd  3913  sbcnestgfw  4387  sbcnestgf  4392  csbnest1g  4398  csbun  4407  csbin  4408  csbdif  4490  csbif  4549  disjors  5093  invdisjrab  5097  disjxiun  5107  disjxun  5108  sbcbr123  5164  eusvnf  5350  reusv2lem4  5359  reusv2  5361  moop2  5465  iunopeqop  5484  pofun  5567  opeliunxp  5708  opeliun2xp  5709  elrnmpt1  5927  resmptf  6013  csbima12  6053  csbcog  6273  fvmpt2f  6972  fvmpts  6974  fvmptdf  6977  fvmpt2i  6981  fvmptex  6985  fmptco  7104  fmptcof  7105  fmptcos  7106  elabrex  7219  elabrexg  7220  fliftfuns  7292  csbov123  7434  ovmpos  7540  fvmpopr2d  7554  ofmpteq  7679  mpomptsx  8046  dmmpossx  8048  fmpox  8049  el2mpocsbcl  8067  offval22  8070  ovmptss  8075  fmpoco  8077  dfmpo  8084  mpoxeldm  8193  mpocurryd  8251  mpocurryvald  8252  fvmpocurryd  8253  eqerlem  8709  qliftfuns  8780  mptelixpg  8911  boxcutc  8917  xpf1o  9109  iunfi  9301  wdom2d  9540  ixpiunwdom  9550  hsmexlem2  10387  ac6c4  10441  iundom2g  10500  seqof2  14032  rlimcld2  15551  nfsum1  15663  sumeq2ii  15666  summolem3  15687  summolem2a  15688  zsum  15691  fsum  15693  sumss2  15699  fsumcvg2  15700  fsumclf  15711  fsumzcl2  15712  fsumsplitf  15715  sumsnf  15716  sumsns  15723  fsummsnunz  15727  fsumsplitsnun  15728  fsum2dlem  15743  fsumcom2  15747  fsumshftm  15754  fsum0diag2  15756  fsum00  15771  fsumabs  15774  fsumrlim  15784  fsumo1  15785  o1fsum  15786  fsumiun  15794  infcvgaux1i  15830  nfcprod1  15881  prodeq2ii  15884  prodmolem3  15906  prodmolem2a  15907  zprod  15910  fprod  15914  fprodntriv  15915  prodss  15920  fprodser  15922  fprodcllemf  15931  prodsn  15935  prodsnf  15937  fprodm1s  15943  fprodp1s  15944  prodsns  15945  fprodabs  15947  fprodn0  15952  fprod2dlem  15953  fprodcom2  15957  fproddivf  15960  fprodsplitf  15961  fprodsplit1f  15963  fprodle  15969  fprodmodd  15970  fprodefsum  16068  sumeven  16364  sumodd  16365  pcmpt  16870  pcmptdvds  16872  natpropd  17948  fucpropd  17949  gsummpt1n0  19902  gsumcom2  19912  gsummptnn0fz  19923  dprd2d2  19983  psrass1lem  21848  mpfrcl  21999  coe1fzgsumdlem  22197  gsummoncoe1  22202  gsumply1eq  22203  evl1gsumdlem  22250  mdetralt2  22503  mdetunilem2  22507  madugsum  22537  fiuncmp  23298  ptcld  23507  ptcldmpt  23508  ptclsg  23509  elmptrab  23721  prdsdsf  24262  prdsxmet  24264  fsumcn  24768  fsum2cn  24769  ovolfiniun  25409  ovoliunlem3  25412  ovoliun  25413  ovoliun2  25414  ovoliunnul  25415  finiunmbl  25452  volfiniun  25455  iundisj  25456  iundisj2  25457  iunmbl  25461  iunmbl2  25465  itgss3  25723  itgfsum  25735  itgabs  25743  limciun  25802  dvmptfsum  25886  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsumrlim  25945  dvfsumrlim2  25946  dvfsum2  25948  itgsubstlem  25962  itgsubst  25963  rlimcnp2  26883  fsumdvdscom  27102  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  fsumvma  27131  dchrisumlema  27406  dchrisumlem2  27408  dchrisumlem3  27409  iunxpssiun1  32504  disjorsf  32516  disjabrex  32518  disjabrexf  32519  iundisjf  32525  iundisj2f  32526  disjunsn  32530  suppss2f  32569  2ndresdju  32580  fmptdF  32587  fmptcof2  32588  acunirnmpt2f  32592  aciunf1lem  32593  funcnv4mpt  32600  f1od2  32651  iundisjfi  32726  iundisj2fi  32727  fsumiunle  32761  gsummpt2co  32995  gsumpart  33004  gsumvsca1  33186  gsumvsca2  33187  rmfsupp2  33196  esumpfinvalf  34073  esum2dlem  34089  esumiun  34091  fiunelros  34171  measiun  34215  voliune  34226  volfiniune  34227  sbcaltop  35976  weiunpo  36460  weiunso  36461  weiunfr  36462  weiunse  36463  bj-sbeqALT  36895  phpreu  37605  finixpnum  37606  ptrest  37620  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  mbfposadd  37668  itgabsnc  37690  ftc1cnnclem  37692  ftc2nc  37703  fsumshftd  38952  riotasv2s  38958  cdleme31sn  40381  cdleme31sn1  40382  cdleme31se2  40384  cdleme32fva  40438  cdleme42b  40479  hlhilset  41935  evl1gprodd  42112  idomnnzgmulnz  42128  deg1gprod  42135  fmpocos  42229  mzpsubst  42743  rabdiophlem2  42797  elnn0rabdioph  42798  dvdsrabdioph  42805  fphpd  42811  monotuz  42937  oddcomabszz  42940  wdom2d2  43031  aomclem6  43055  flcidc  43166  fsumcnf  45022  sumsnd  45027  fiiuncl  45066  eliin2f  45105  disjf1  45184  disjrnmpt2  45189  disjinfi  45193  fmptf  45240  fmptff  45270  iuneqfzuzlem  45337  supxrleubrnmptf  45454  fsummulc1f  45576  fsumnncl  45577  fsumf1of  45579  fsumiunss  45580  fsumreclf  45581  fsumlessf  45582  fprodexp  45599  fprodabs2  45600  mccllem  45602  fprodcnlem  45604  fprodcn  45605  climeldmeqmpt  45673  climeldmeqmpt3  45694  climinf2mpt  45719  climinfmpt  45720  limsupequzmptf  45736  fprodcncf  45905  dvmptmulf  45942  dvnmptdivc  45943  dvmptfprod  45950  iblsplitf  45975  fourierdlem86  46197  fourierdlem112  46223  sge0f1o  46387  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0ltfirpmpt2  46431  sge0isummpt2  46437  sge0xaddlem2  46439  sge0xadd  46440  hoimbl2  46670  vonn0ioo2  46695  vonn0icc2  46697  csbafv12g  47142  csbaovg  47185  csbafv212g  47224  fsummsndifre  47377  fsumsplitsndif  47378  fsummmodsndifre  47379  fsummmodsnunz  47380  dmmpossx2  48329