Theorem nfcsb1v 3852

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

Syntax hints:  Ⅎwnfc 2936  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-sbc 3721  df-csb 3829

This theorem is referenced by:  csbhypf  3856  csbiebt  3857  cbvrabcsfw  3869  cbvralcsf  3870  cbvreucsf  3872  cbvrabcsf  3873  rspc2vd  3877  sbcnestgfw  4326  sbcnestgf  4331  csbnest1g  4337  csbun  4346  csbin  4347  csbif  4480  disjors  5011  invdisjrabw  5015  invdisjrab  5016  disjxiun  5027  disjxun  5028  sbcbr123  5084  eusvnf  5258  reusv2lem4  5267  reusv2  5269  moop2  5357  iunopeqop  5376  pofun  5455  opeliunxp  5583  elrnmpt1  5794  resmptf  5874  csbima12  5914  fvmpt2f  6746  fvmpts  6748  fvmptdf  6751  fvmpt2i  6755  fvmptex  6759  fmptco  6868  fmptcof  6869  fmptcos  6870  elabrex  6980  fliftfuns  7046  csbov123  7177  ovmpos  7277  fvmpopr2d  7290  ofmpteq  7408  mpomptsx  7744  dmmpossx  7746  fmpox  7747  el2mpocsbcl  7763  offval22  7766  ovmptss  7771  fmpoco  7773  dfmpo  7780  mpoxeldm  7860  mpocurryd  7918  mpocurryvald  7919  fvmpocurryd  7920  eqerlem  8306  qliftfuns  8367  mptelixpg  8482  boxcutc  8488  xpf1o  8663  iunfi  8796  wdom2d  9028  ixpiunwdom  9038  hsmexlem2  9838  ac6c4  9892  iundom2g  9951  seqof2  13424  rlimcld2  14927  nfsum1  15038  sumeq2ii  15042  summolem3  15063  summolem2a  15064  zsum  15067  fsum  15069  sumss2  15075  fsumcvg2  15076  fsumzcl2  15087  fsumsplitf  15090  sumsnf  15091  sumsns  15097  fsummsnunz  15101  fsumsplitsnun  15102  fsum2dlem  15117  fsumcom2  15121  fsumshftm  15128  fsum0diag2  15130  fsum00  15145  fsumabs  15148  fsumrlim  15158  fsumo1  15159  o1fsum  15160  fsumiun  15168  infcvgaux1i  15204  nfcprod1  15256  prodeq2ii  15259  prodmolem3  15279  prodmolem2a  15280  zprod  15283  fprod  15287  fprodntriv  15288  prodss  15293  fprodser  15295  fprodcllemf  15304  prodsn  15308  prodsnf  15310  fprodm1s  15316  fprodp1s  15317  prodsns  15318  fprodabs  15320  fprodn0  15325  fprod2dlem  15326  fprodcom2  15330  fproddivf  15333  fprodsplitf  15334  fprodsplit1f  15336  fprodle  15342  fprodmodd  15343  fprodefsum  15440  sumeven  15728  sumodd  15729  pcmpt  16218  pcmptdvds  16220  natpropd  17238  fucpropd  17239  gsummpt1n0  19078  gsumcom2  19088  gsummptnn0fz  19099  dprd2d2  19159  psrass1lem  20615  mpfrcl  20757  coe1fzgsumdlem  20930  gsummoncoe1  20933  gsumply1eq  20934  evl1gsumdlem  20980  mdetralt2  21214  mdetunilem2  21218  madugsum  21248  fiuncmp  22009  ptcld  22218  ptcldmpt  22219  ptclsg  22220  elmptrab  22432  prdsdsf  22974  prdsxmet  22976  fsumcn  23475  fsum2cn  23476  ovolfiniun  24105  ovoliunlem3  24108  ovoliun  24109  ovoliun2  24110  ovoliunnul  24111  finiunmbl  24148  volfiniun  24151  iundisj  24152  iundisj2  24153  iunmbl  24157  iunmbl2  24161  itgss3  24418  itgfsum  24430  itgabs  24438  limciun  24497  dvmptfsum  24578  dvfsumle  24624  dvfsumabs  24626  dvfsumlem1  24629  dvfsumlem2  24630  dvfsumlem3  24631  dvfsumlem4  24632  dvfsumrlim  24634  dvfsumrlim2  24635  dvfsum2  24637  itgsubstlem  24651  itgsubst  24652  rlimcnp2  25552  fsumdvdscom  25770  fsumdvdsmul  25780  fsumvma  25797  dchrisumlema  26072  dchrisumlem2  26074  dchrisumlem3  26075  disjorsf  30343  disjabrex  30345  disjabrexf  30346  iundisjf  30352  iundisj2f  30353  disjunsn  30357  suppss2f  30398  2ndresdju  30411  fmptdF  30419  fmptcof2  30420  acunirnmpt2f  30424  aciunf1lem  30425  funcnv4mpt  30432  f1od2  30483  iundisjfi  30545  iundisj2fi  30546  fsumiunle  30571  gsummpt2co  30733  gsumpart  30740  gsumvsca1  30904  gsumvsca2  30905  rmfsupp2  30917  esumpfinvalf  31445  esum2dlem  31461  esumiun  31463  fiunelros  31543  measiun  31587  voliune  31598  volfiniune  31599  sbcaltop  33555  bj-sbeqALT  34341  csbdif  34742  phpreu  35041  finixpnum  35042  ptrest  35056  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem28  35085  mbfposadd  35104  itgabsnc  35126  ftc1cnnclem  35128  ftc2nc  35139  fsumshftd  36248  riotasv2s  36254  cdleme31sn  37676  cdleme31sn1  37677  cdleme31se2  37679  cdleme32fva  37733  cdleme42b  37774  hlhilset  39230  mzpsubst  39689  rabdiophlem2  39743  elnn0rabdioph  39744  dvdsrabdioph  39751  fphpd  39757  monotuz  39882  oddcomabszz  39885  wdom2d2  39976  aomclem6  40003  flcidc  40118  csbcog  40350  fsumcnf  41650  sumsnd  41655  elabrexg  41675  fiiuncl  41699  eliin2f  41740  disjf1  41809  disjrnmpt2  41815  disjinfi  41820  fmptf  41875  iuneqfzuzlem  41966  supxrleubrnmptf  42090  fsumclf  42211  fsummulc1f  42212  fsumnncl  42213  fsumf1of  42216  fsumiunss  42217  fsumreclf  42218  fsumlessf  42219  fprodexp  42236  fprodabs2  42237  mccllem  42239  fprodcnlem  42241  fprodcn  42242  climeldmeqmpt  42310  climeldmeqmpt3  42331  climinf2mpt  42356  climinfmpt  42357  limsupequzmptf  42373  fprodcncf  42542  dvmptmulf  42579  dvnmptdivc  42580  dvmptfprod  42587  iblsplitf  42612  fourierdlem86  42834  fourierdlem112  42860  sge0iunmptlemfi  43052  sge0iunmptlemre  43054  sge0iunmpt  43057  sge0ltfirpmpt2  43065  sge0isummpt2  43071  sge0xaddlem2  43073  sge0xadd  43074  hoimbl2  43304  vonn0ioo2  43329  vonn0icc2  43331  csbafv12g  43693  csbaovg  43736  csbafv212g  43775  fsummsndifre  43889  fsumsplitsndif  43890  fsummmodsndifre  43891  fsummmodsnunz  43892  opeliun2xp  44734  dmmpossx2  44738