Theorem nfcsb1v 3932

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

Syntax hints:  Ⅎwnfc 2887  ⦋csb 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-sbc 3791  df-csb 3908

This theorem is referenced by:  csbhypf  3936  csbiebt  3937  cbvrabcsfw  3951  cbvralcsf  3952  cbvreucsf  3954  cbvrabcsf  3955  rspc2vd  3958  sbcnestgfw  4426  sbcnestgf  4431  csbnest1g  4437  csbun  4446  csbin  4447  csbdif  4529  csbif  4587  disjors  5130  invdisjrab  5134  disjxiun  5144  disjxun  5145  sbcbr123  5201  eusvnf  5397  reusv2lem4  5406  reusv2  5408  moop2  5511  iunopeqop  5530  pofun  5614  opeliunxp  5755  elrnmpt1  5973  resmptf  6058  csbima12  6098  csbcog  6318  fvmpt2f  7016  fvmpts  7018  fvmptdf  7021  fvmpt2i  7025  fvmptex  7029  fmptco  7148  fmptcof  7149  fmptcos  7150  elabrex  7261  elabrexg  7262  fliftfuns  7333  csbov123  7474  ovmpos  7580  fvmpopr2d  7594  ofmpteq  7719  mpomptsx  8087  dmmpossx  8089  fmpox  8090  el2mpocsbcl  8108  offval22  8111  ovmptss  8116  fmpoco  8118  dfmpo  8125  mpoxeldm  8234  mpocurryd  8292  mpocurryvald  8293  fvmpocurryd  8294  eqerlem  8778  qliftfuns  8842  mptelixpg  8973  boxcutc  8979  xpf1o  9177  iunfi  9380  wdom2d  9617  ixpiunwdom  9627  hsmexlem2  10464  ac6c4  10518  iundom2g  10577  seqof2  14097  rlimcld2  15610  nfsum1  15722  sumeq2ii  15725  summolem3  15746  summolem2a  15747  zsum  15750  fsum  15752  sumss2  15758  fsumcvg2  15759  fsumclf  15770  fsumzcl2  15771  fsumsplitf  15774  sumsnf  15775  sumsns  15782  fsummsnunz  15786  fsumsplitsnun  15787  fsum2dlem  15802  fsumcom2  15806  fsumshftm  15813  fsum0diag2  15815  fsum00  15830  fsumabs  15833  fsumrlim  15843  fsumo1  15844  o1fsum  15845  fsumiun  15853  infcvgaux1i  15889  nfcprod1  15940  prodeq2ii  15943  prodmolem3  15965  prodmolem2a  15966  zprod  15969  fprod  15973  fprodntriv  15974  prodss  15979  fprodser  15981  fprodcllemf  15990  prodsn  15994  prodsnf  15996  fprodm1s  16002  fprodp1s  16003  prodsns  16004  fprodabs  16006  fprodn0  16011  fprod2dlem  16012  fprodcom2  16016  fproddivf  16019  fprodsplitf  16020  fprodsplit1f  16022  fprodle  16028  fprodmodd  16029  fprodefsum  16127  sumeven  16420  sumodd  16421  pcmpt  16925  pcmptdvds  16927  natpropd  18032  fucpropd  18033  gsummpt1n0  19997  gsumcom2  20007  gsummptnn0fz  20018  dprd2d2  20078  psrass1lem  21969  mpfrcl  22126  coe1fzgsumdlem  22322  gsummoncoe1  22327  gsumply1eq  22328  evl1gsumdlem  22375  mdetralt2  22630  mdetunilem2  22634  madugsum  22664  fiuncmp  23427  ptcld  23636  ptcldmpt  23637  ptclsg  23638  elmptrab  23850  prdsdsf  24392  prdsxmet  24394  fsumcn  24907  fsum2cn  24908  ovolfiniun  25549  ovoliunlem3  25552  ovoliun  25553  ovoliun2  25554  ovoliunnul  25555  finiunmbl  25592  volfiniun  25595  iundisj  25596  iundisj2  25597  iunmbl  25601  iunmbl2  25605  itgss3  25864  itgfsum  25876  itgabs  25884  limciun  25943  dvmptfsum  26027  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsumrlim  26086  dvfsumrlim2  26087  dvfsum2  26089  itgsubstlem  26103  itgsubst  26104  rlimcnp2  27023  fsumdvdscom  27242  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  fsumvma  27271  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  disjorsf  32599  disjabrex  32601  disjabrexf  32602  iundisjf  32608  iundisj2f  32609  disjunsn  32613  suppss2f  32654  2ndresdju  32665  fmptdF  32672  fmptcof2  32673  acunirnmpt2f  32677  aciunf1lem  32678  funcnv4mpt  32685  f1od2  32738  iundisjfi  32803  iundisj2fi  32804  fsumiunle  32835  gsummpt2co  33033  gsumpart  33042  gsumvsca1  33214  gsumvsca2  33215  rmfsupp2  33227  esumpfinvalf  34056  esum2dlem  34072  esumiun  34074  fiunelros  34154  measiun  34198  voliune  34209  volfiniune  34210  sbcaltop  35962  weiunpo  36447  weiunso  36448  weiunfr  36449  weiunse  36450  bj-sbeqALT  36882  phpreu  37590  finixpnum  37591  ptrest  37605  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  mbfposadd  37653  itgabsnc  37675  ftc1cnnclem  37677  ftc2nc  37688  fsumshftd  38933  riotasv2s  38939  cdleme31sn  40362  cdleme31sn1  40363  cdleme31se2  40365  cdleme32fva  40419  cdleme42b  40460  hlhilset  41916  evl1gprodd  42098  idomnnzgmulnz  42114  deg1gprod  42121  fmpocos  42253  mzpsubst  42735  rabdiophlem2  42789  elnn0rabdioph  42790  dvdsrabdioph  42797  fphpd  42803  monotuz  42929  oddcomabszz  42932  wdom2d2  43023  aomclem6  43047  flcidc  43158  fsumcnf  44958  sumsnd  44963  fiiuncl  45004  eliin2f  45043  disjf1  45125  disjrnmpt2  45130  disjinfi  45134  fmptf  45182  fmptff  45214  iuneqfzuzlem  45283  supxrleubrnmptf  45400  fsummulc1f  45526  fsumnncl  45527  fsumf1of  45529  fsumiunss  45530  fsumreclf  45531  fsumlessf  45532  fprodexp  45549  fprodabs2  45550  mccllem  45552  fprodcnlem  45554  fprodcn  45555  climeldmeqmpt  45623  climeldmeqmpt3  45644  climinf2mpt  45669  climinfmpt  45670  limsupequzmptf  45686  fprodcncf  45855  dvmptmulf  45892  dvnmptdivc  45893  dvmptfprod  45900  iblsplitf  45925  fourierdlem86  46147  fourierdlem112  46173  sge0f1o  46337  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0ltfirpmpt2  46381  sge0isummpt2  46387  sge0xaddlem2  46389  sge0xadd  46390  hoimbl2  46620  vonn0ioo2  46645  vonn0icc2  46647  csbafv12g  47086  csbaovg  47129  csbafv212g  47168  fsummsndifre  47296  fsumsplitsndif  47297  fsummmodsndifre  47298  fsummmodsnunz  47299  opeliun2xp  48177  dmmpossx2  48181