Theorem nfcsb1v 3857

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

Syntax hints:  Ⅎwnfc 2888  ⦋csb 3833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-sbc 3726  df-csb 3834

This theorem is referenced by:  csbhypf  3861  csbiebt  3862  cbvrabcsfw  3874  cbvralcsf  3875  cbvreucsf  3877  cbvrabcsf  3878  rspc2vd  3881  sbcnestgfw  4352  sbcnestgf  4357  csbnest1g  4363  csbun  4372  csbin  4373  csbdif  4456  csbif  4515  disjors  5058  invdisjrab  5062  disjxiun  5072  disjxun  5073  sbcbr123  5129  eusvnf  5324  reusv2lem4  5333  reusv2  5335  moop2  5446  iunopeqop  5465  iunopeqopOLD  5466  pofun  5547  opeliunxp  5688  opeliun2xp  5689  elrnmpt1  5909  resmptf  5998  csbima12  6038  csbcog  6252  fvmpt2f  6940  fvmpts  6943  fvmptdf  6946  fvmpt2i  6950  fvmptex  6954  fmptco  7075  fmptcof  7076  fmptcos  7077  elabrex  7190  elabrexg  7191  fliftfuns  7262  csbov123  7404  ovmpos  7508  fvmpopr2d  7522  ofmpteq  7647  mpomptsx  8010  dmmpossx  8012  fmpox  8013  el2mpocsbcl  8028  offval22  8031  ovmptss  8036  fmpoco  8038  dfmpo  8045  mpoxeldm  8155  mpocurryd  8213  mpocurryvald  8214  fvmpocurryd  8215  eqerlem  8673  qliftfuns  8745  mptelixpg  8877  boxcutc  8883  xpf1o  9071  iunfi  9247  wdom2d  9489  ixpiunwdom  9499  hsmexlem2  10344  ac6c4  10398  iundom2g  10457  seqof2  14017  rlimcld2  15535  nfsum1  15647  sumeq2ii  15650  summolem3  15671  summolem2a  15672  zsum  15675  fsum  15677  sumss2  15683  fsumcvg2  15684  fsumclf  15695  fsumzcl2  15696  fsumsplitf  15699  sumsnf  15700  sumsns  15707  fsummsnunz  15711  fsumsplitsnun  15712  fsum2dlem  15727  fsumcom2  15731  fsumshftm  15738  fsum0diag2  15740  fsum00  15756  fsumabs  15759  fsumrlim  15769  fsumo1  15770  o1fsum  15771  fsumiun  15779  infcvgaux1i  15817  nfcprod1  15868  prodeq2ii  15871  prodmolem3  15893  prodmolem2a  15894  zprod  15897  fprod  15901  fprodntriv  15902  prodss  15907  fprodser  15909  fprodcllemf  15918  prodsn  15922  prodsnf  15924  fprodm1s  15930  fprodp1s  15931  prodsns  15932  fprodabs  15934  fprodn0  15939  fprod2dlem  15940  fprodcom2  15944  fproddivf  15947  fprodsplitf  15948  fprodsplit1f  15950  fprodle  15956  fprodmodd  15957  fprodefsum  16055  sumeven  16351  sumodd  16352  pcmpt  16858  pcmptdvds  16860  natpropd  17941  fucpropd  17942  gsummpt1n0  19935  gsumcom2  19945  gsummptnn0fz  19956  dprd2d2  20016  psrass1lem  21912  mpfrcl  22065  coe1fzgsumdlem  22293  gsummoncoe1  22298  gsumply1eq  22299  evl1gsumdlem  22346  mdetralt2  22596  mdetunilem2  22600  madugsum  22630  fiuncmp  23391  ptcld  23600  ptcldmpt  23601  ptclsg  23602  elmptrab  23814  prdsdsf  24354  prdsxmet  24356  fsumcn  24859  fsum2cn  24860  ovolfiniun  25490  ovoliunlem3  25493  ovoliun  25494  ovoliun2  25495  ovoliunnul  25496  finiunmbl  25533  volfiniun  25536  iundisj  25537  iundisj2  25538  iunmbl  25542  iunmbl2  25546  itgss3  25804  itgfsum  25816  itgabs  25824  limciun  25883  dvmptfsum  25964  dvfsumle  26010  dvfsumabs  26012  dvfsumlem1  26015  dvfsumlem2  26016  dvfsumlem3  26017  dvfsumlem4  26018  dvfsumrlim  26020  dvfsumrlim2  26021  dvfsum2  26023  itgsubstlem  26037  itgsubst  26038  rlimcnp2  26952  fsumdvdscom  27170  fsumdvdsmul  27180  fsumvma  27198  dchrisumlema  27473  dchrisumlem2  27475  dchrisumlem3  27476  iunxpssiun1  32661  disjorsf  32673  disjabrex  32675  disjabrexf  32676  iundisjf  32682  iundisj2f  32683  disjunsn  32687  suppss2f  32734  2ndresdju  32745  fmptdF  32752  fmptcof2  32753  acunirnmpt2f  32757  aciunf1lem  32758  funcnv4mpt  32764  f1od2  32815  iundisjfi  32892  iundisj2fi  32893  fsumiunle  32925  gsummpt2co  33133  gsummptp1  33142  gsumpart  33148  gsumvsca1  33311  gsumvsca2  33312  rmfsupp2  33323  esumpfinvalf  34272  esum2dlem  34288  esumiun  34290  fiunelros  34370  measiun  34414  voliune  34425  volfiniune  34426  sbcaltop  36224  weiunpo  36708  weiunso  36709  weiunfr  36710  weiunse  36711  csbttc  36752  bj-sbeqALT  37268  phpreu  37986  finixpnum  37987  ptrest  38001  poimirlem23  38025  poimirlem24  38026  poimirlem25  38027  poimirlem26  38028  poimirlem27  38029  poimirlem28  38030  mbfposadd  38049  itgabsnc  38071  ftc1cnnclem  38073  ftc2nc  38084  fsumshftd  39459  riotasv2s  39465  cdleme31sn  40887  cdleme31sn1  40888  cdleme31se2  40890  cdleme32fva  40944  cdleme42b  40985  hlhilset  42441  evl1gprodd  42617  idomnnzgmulnz  42633  deg1gprod  42640  fmpocos  42735  mzpsubst  43212  rabdiophlem2  43262  elnn0rabdioph  43263  dvdsrabdioph  43270  fphpd  43276  monotuz  43401  oddcomabszz  43404  wdom2d2  43495  aomclem6  43519  flcidc  43630  fsumcnf  45484  sumsnd  45489  fiiuncl  45528  eliin2f  45565  disjf1  45644  disjrnmpt2  45649  disjinfi  45653  fmptf  45697  fmptff  45727  iuneqfzuzlem  45793  supxrleubrnmptf  45908  fsummulc1f  46030  fsumnncl  46031  fsumf1of  46033  fsumiunss  46034  fsumreclf  46035  fsumlessf  46036  fprodexp  46053  fprodabs2  46054  mccllem  46056  fprodcnlem  46058  fprodcn  46059  climeldmeqmpt  46125  climeldmeqmpt3  46146  climinf2mpt  46171  climinfmpt  46172  limsupequzmptf  46188  fprodcncf  46357  dvmptmulf  46394  dvnmptdivc  46395  dvmptfprod  46402  iblsplitf  46427  fourierdlem86  46649  fourierdlem112  46675  sge0f1o  46839  sge0iunmptlemfi  46870  sge0iunmptlemre  46872  sge0iunmpt  46875  sge0ltfirpmpt2  46883  sge0isummpt2  46889  sge0xaddlem2  46891  sge0xadd  46892  hoimbl2  47122  vonn0ioo2  47147  vonn0icc2  47149  csbafv12g  47614  csbaovg  47657  csbafv212g  47696  fsummsndifre  47857  fsumsplitsndif  47858  fsummmodsndifre  47859  fsummmodsnunz  47860  dmmpossx2  48842