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

Syntax hints:  Ⅎwnfc 2879  ⦋csb 3850

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-sbc 3742  df-csb 3851

This theorem is referenced by:  csbhypf  3878  csbiebt  3879  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  rspc2vd  3898  sbcnestgfw  4371  sbcnestgf  4376  csbnest1g  4382  csbun  4391  csbin  4392  csbdif  4474  csbif  4533  disjors  5074  invdisjrab  5078  disjxiun  5088  disjxun  5089  sbcbr123  5145  eusvnf  5330  reusv2lem4  5339  reusv2  5341  moop2  5442  iunopeqop  5461  pofun  5542  opeliunxp  5683  opeliun2xp  5684  elrnmpt1  5900  resmptf  5988  csbima12  6028  csbcog  6244  fvmpt2f  6930  fvmpts  6932  fvmptdf  6935  fvmpt2i  6939  fvmptex  6943  fmptco  7062  fmptcof  7063  fmptcos  7064  elabrex  7176  elabrexg  7177  fliftfuns  7248  csbov123  7390  ovmpos  7494  fvmpopr2d  7508  ofmpteq  7633  mpomptsx  7996  dmmpossx  7998  fmpox  7999  el2mpocsbcl  8015  offval22  8018  ovmptss  8023  fmpoco  8025  dfmpo  8032  mpoxeldm  8141  mpocurryd  8199  mpocurryvald  8200  fvmpocurryd  8201  eqerlem  8657  qliftfuns  8728  mptelixpg  8859  boxcutc  8865  xpf1o  9052  iunfi  9227  wdom2d  9466  ixpiunwdom  9476  hsmexlem2  10318  ac6c4  10372  iundom2g  10431  seqof2  13967  rlimcld2  15485  nfsum1  15597  sumeq2ii  15600  summolem3  15621  summolem2a  15622  zsum  15625  fsum  15627  sumss2  15633  fsumcvg2  15634  fsumclf  15645  fsumzcl2  15646  fsumsplitf  15649  sumsnf  15650  sumsns  15657  fsummsnunz  15661  fsumsplitsnun  15662  fsum2dlem  15677  fsumcom2  15681  fsumshftm  15688  fsum0diag2  15690  fsum00  15705  fsumabs  15708  fsumrlim  15718  fsumo1  15719  o1fsum  15720  fsumiun  15728  infcvgaux1i  15764  nfcprod1  15815  prodeq2ii  15818  prodmolem3  15840  prodmolem2a  15841  zprod  15844  fprod  15848  fprodntriv  15849  prodss  15854  fprodser  15856  fprodcllemf  15865  prodsn  15869  prodsnf  15871  fprodm1s  15877  fprodp1s  15878  prodsns  15879  fprodabs  15881  fprodn0  15886  fprod2dlem  15887  fprodcom2  15891  fproddivf  15894  fprodsplitf  15895  fprodsplit1f  15897  fprodle  15903  fprodmodd  15904  fprodefsum  16002  sumeven  16298  sumodd  16299  pcmpt  16804  pcmptdvds  16806  natpropd  17886  fucpropd  17887  gsummpt1n0  19878  gsumcom2  19888  gsummptnn0fz  19899  dprd2d2  19959  psrass1lem  21870  mpfrcl  22021  coe1fzgsumdlem  22219  gsummoncoe1  22224  gsumply1eq  22225  evl1gsumdlem  22272  mdetralt2  22525  mdetunilem2  22529  madugsum  22559  fiuncmp  23320  ptcld  23529  ptcldmpt  23530  ptclsg  23531  elmptrab  23743  prdsdsf  24283  prdsxmet  24285  fsumcn  24789  fsum2cn  24790  ovolfiniun  25430  ovoliunlem3  25433  ovoliun  25434  ovoliun2  25435  ovoliunnul  25436  finiunmbl  25473  volfiniun  25476  iundisj  25477  iundisj2  25478  iunmbl  25482  iunmbl2  25486  itgss3  25744  itgfsum  25756  itgabs  25764  limciun  25823  dvmptfsum  25907  dvfsumle  25954  dvfsumleOLD  25955  dvfsumabs  25957  dvfsumlem1  25960  dvfsumlem2  25961  dvfsumlem2OLD  25962  dvfsumlem3  25963  dvfsumlem4  25964  dvfsumrlim  25966  dvfsumrlim2  25967  dvfsum2  25969  itgsubstlem  25983  itgsubst  25984  rlimcnp2  26904  fsumdvdscom  27123  fsumdvdsmul  27133  fsumdvdsmulOLD  27135  fsumvma  27152  dchrisumlema  27427  dchrisumlem2  27429  dchrisumlem3  27430  iunxpssiun1  32546  disjorsf  32558  disjabrex  32560  disjabrexf  32561  iundisjf  32567  iundisj2f  32568  disjunsn  32572  suppss2f  32618  2ndresdju  32629  fmptdF  32636  fmptcof2  32637  acunirnmpt2f  32641  aciunf1lem  32642  funcnv4mpt  32649  f1od2  32700  iundisjfi  32776  iundisj2fi  32777  fsumiunle  32810  gsummpt2co  33026  gsumpart  33035  gsumvsca1  33193  gsumvsca2  33194  rmfsupp2  33203  esumpfinvalf  34087  esum2dlem  34103  esumiun  34105  fiunelros  34185  measiun  34229  voliune  34240  volfiniune  34241  sbcaltop  36021  weiunpo  36505  weiunso  36506  weiunfr  36507  weiunse  36508  bj-sbeqALT  36940  phpreu  37650  finixpnum  37651  ptrest  37665  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  poimirlem28  37694  mbfposadd  37713  itgabsnc  37735  ftc1cnnclem  37737  ftc2nc  37748  fsumshftd  38997  riotasv2s  39003  cdleme31sn  40425  cdleme31sn1  40426  cdleme31se2  40428  cdleme32fva  40482  cdleme42b  40523  hlhilset  41979  evl1gprodd  42156  idomnnzgmulnz  42172  deg1gprod  42179  fmpocos  42273  mzpsubst  42787  rabdiophlem2  42841  elnn0rabdioph  42842  dvdsrabdioph  42849  fphpd  42855  monotuz  42980  oddcomabszz  42983  wdom2d2  43074  aomclem6  43098  flcidc  43209  fsumcnf  45064  sumsnd  45069  fiiuncl  45108  eliin2f  45147  disjf1  45226  disjrnmpt2  45231  disjinfi  45235  fmptf  45282  fmptff  45312  iuneqfzuzlem  45379  supxrleubrnmptf  45495  fsummulc1f  45617  fsumnncl  45618  fsumf1of  45620  fsumiunss  45621  fsumreclf  45622  fsumlessf  45623  fprodexp  45640  fprodabs2  45641  mccllem  45643  fprodcnlem  45645  fprodcn  45646  climeldmeqmpt  45712  climeldmeqmpt3  45733  climinf2mpt  45758  climinfmpt  45759  limsupequzmptf  45775  fprodcncf  45944  dvmptmulf  45981  dvnmptdivc  45982  dvmptfprod  45989  iblsplitf  46014  fourierdlem86  46236  fourierdlem112  46262  sge0f1o  46426  sge0iunmptlemfi  46457  sge0iunmptlemre  46459  sge0iunmpt  46462  sge0ltfirpmpt2  46470  sge0isummpt2  46476  sge0xaddlem2  46478  sge0xadd  46479  hoimbl2  46709  vonn0ioo2  46734  vonn0icc2  46736  csbafv12g  47174  csbaovg  47217  csbafv212g  47256  fsummsndifre  47409  fsumsplitsndif  47410  fsummmodsndifre  47411  fsummmodsnunz  47412  dmmpossx2  48374