Theorem nfcsb1v 3870

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

This proof depends on syntax axioms:  Ⅎwnfc 2907  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-sbc 3739  df-csb 3847

This theorem is used by:  csbhypf  3874  csbiebt  3875  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  rspc2vd  3894  sbcnestgfw  4378  sbcnestgf  4383  csbnest1g  4389  csbun  4398  csbin  4399  csbdif  4480  csbif  4539  disjors  5085  invdisjrab  5089  disjxiun  5099  disjxun  5100  sbcbr123  5159  eusvnf  5353  reusv2lem4  5362  reusv2  5364  moop2  5473  iunopeqop  5493  iunopeqopOLD  5494  pofun  5576  opeliunxp  5717  opeliun2xp  5718  elrnmpt1  5941  resmptf  6030  csbima12  6075  csbcog  6300  fvmpt2f  6995  fvmpts  6998  fvmptdf  7001  fvmpt2i  7005  fvmptex  7009  fmptco  7131  fmptcof  7132  fmptcos  7133  elabrex  7247  elabrexg  7248  fliftfuns  7323  csbov123  7465  ovmpos  7569  fvmpopr2d  7583  ofmpteq  7717  mpomptsx  8076  dmmpossx  8078  fmpox  8079  el2mpocsbcl  8097  offval22  8100  ovmptssOLD  8106  fmpoco  8108  f1od2  8111  dfmpo  8116  mpoxeldm  8232  mpocurryd  8290  mpocurryvald  8291  fvmpocurryd  8292  eqerlem  8757  qliftfuns  8829  mptelixpg  8967  boxcutc  8973  xpf1o  9162  iunfi  9336  wdom2d  9578  ixpiunwdom  9588  hsmexlem2  10509  ac6c4  10563  iundom2g  10628  seqof2  14207  rlimcld2  15751  nfsum1  15863  sumeq2ii  15866  summolem3  15886  summolem2a  15887  zsum  15890  fsum  15892  sumss2  15898  fsumcvg2  15899  fsumclf  15910  fsumzcl2  15911  fsumsplitf  15914  sumsnf  15915  sumsns  15922  fsummsnunz  15926  fsumsplitsnun  15927  fsum2dlem  15942  fsumcom2  15946  fsumshftm  15953  fsum0diag2  15955  fsum00  15971  fsumabs  15974  fsumrlim  15984  fsumo1  15985  o1fsum  15986  fsumiun  15994  infcvgaux1i  16032  nfcprod1  16083  prodeq2ii  16086  prodmolem3  16106  prodmolem2a  16107  zprod  16110  fprod  16114  fprodntriv  16115  prodss  16120  fprodser  16122  fprodcllemf  16131  prodsn  16135  prodsnf  16137  fprodm1s  16143  fprodp1s  16144  prodsns  16145  fprodabs  16147  fprodn0  16152  fprod2dlem  16153  fprodcom2  16157  fproddivf  16160  fprodsplitf  16161  fprodsplit1f  16163  fprodle  16169  fprodmodd  16170  fprodefsum  16267  sumeven  16563  sumodd  16564  pcmpt  17076  pcmptdvds  17078  natpropd  18160  fucpropd  18161  gsummpt1n0  20185  gsumcom2  20195  gsummptnn0fz  20206  dprd2d2  20266  psrass1lem  22247  mpfrcl  22400  coe1fzgsumdlem  22627  gsummoncoe1  22632  gsumply1eq  22633  evl1gsumdlem  22680  mdetralt2  22930  mdetunilem2  22934  madugsum  22964  fiuncmp  23728  ptcld  23938  ptcldmpt  23939  ptclsg  23940  elmptrab  24152  prdsdsf  24692  prdsxmet  24694  fsumcn  25197  fsum2cn  25198  ovolfiniun  25828  ovoliunlem3  25831  ovoliun  25832  ovoliun2  25833  ovoliunnul  25834  finiunmbl  25871  volfiniun  25874  iundisj  25875  iundisj2  25876  iunmbl  25880  iunmbl2  25884  itgss3  26141  itgfsum  26153  itgabs  26161  limciun  26220  dvmptfsum  26301  dvfsumle  26347  dvfsumabs  26349  dvfsumlem1  26352  dvfsumlem2  26353  dvfsumlem3  26354  dvfsumlem4  26355  dvfsumrlim  26357  dvfsumrlim2  26358  dvfsum2  26360  itgsubstlem  26374  itgsubst  26375  rlimcnp2  27300  fsumdvdscom  27518  fsumdvdsmul  27528  fsumvma  27546  dchrisumlema  27821  dchrisumlem2  27823  dchrisumlem3  27824  iunxpssiun1  33210  disjorsf  33222  disjabrex  33224  disjabrexf  33225  iundisjf  33231  iundisj2f  33232  disjunsn  33236  suppss2f  33280  2ndresdju  33291  fmptdf2  33298  fmptcof2  33299  acunirnmpt2f  33303  aciunf1lem  33304  funcnv4mpt  33310  iundisjfi  33435  iundisj2fi  33436  fsumiunle  33467  gsummpt2co  33656  gsummptp1  33665  gsumpart  33671  gsumvsca1  33834  gsumvsca2  33835  rmfsupp2  33845  esumpfinvalf  34755  esum2dlem  34771  esumiun  34773  fiunelros  34854  measiun  34898  voliune  34909  volfiniune  34910  sbcaltop  36839  weiunpo  37346  weiunso  37347  weiunfr  37348  weiunse  37349  csbttc  37390  bj-sbeqALT  37905  phpreu  38621  finixpnum  38622  ptrest  38631  poimirlem23  38655  poimirlem24  38656  poimirlem25  38657  poimirlem26  38658  poimirlem27  38659  poimirlem28  38660  mbfposadd  38679  itgabsnc  38701  ftc1cnnclem  38703  ftc2nc  38714  fsumshftd  40103  riotasv2s  40109  cdleme31sn  41531  cdleme31sn1  41532  cdleme31se2  41534  cdleme32fva  41588  cdleme42b  41629  hlhilset  43085  evl1gprodd  43261  idomnnzgmulnz  43277  deg1gprod  43284  fmpocos  43381  mzpsubst  43853  rabdiophlem2  43903  elnn0rabdioph  43904  dvdsrabdioph  43911  fphpd  43917  monotuz  44042  oddcomabszz  44045  wdom2d2  44136  aomclem6  44155  flcidc  44266  fsumcnf  46132  sumsnd  46137  fiiuncl  46176  eliin2f  46213  disjf1  46292  disjrnmpt2  46297  disjinfi  46301  fmptf  46345  fmptff  46375  iuneqfzuzlem  46440  supxrleubrnmptf  46555  fsummulc1f  46677  fsumnncl  46678  fsumf1of  46680  fsumiunss  46681  fsumreclf  46682  fsumlessf  46683  fprodexp  46700  fprodabs2  46701  mccllem  46703  fprodcnlem  46705  fprodcn  46706  climeldmeqmpt  46772  climeldmeqmpt3  46793  climinf2mpt  46818  climinfmpt  46819  limsupequzmptf  46835  fprodcncf  47004  dvmptmulf  47041  dvnmptdivc  47042  dvmptfprod  47049  iblsplitf  47074  fourierdlem86  47296  fourierdlem112  47322  sge0f1o  47486  sge0iunmptlemfi  47517  sge0iunmptlemre  47519  sge0iunmpt  47522  sge0ltfirpmpt2  47530  sge0isummpt2  47536  sge0xaddlem2  47538  sge0xadd  47539  hoimbl2  47769  vonn0ioo2  47794  vonn0icc2  47796  csbafv12g  48301  csbaovg  48344  csbafv212g  48383  fsummsndifre  48544  fsumsplitsndif  48545  fsummmodsndifre  48546  fsummmodsnunz  48547  dmmpossx2  49543