Theorem nfcsb1v 3915

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

Syntax hints:  Ⅎwnfc 2879  ⦋csb 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-sbc 3776  df-csb 3891

This theorem is referenced by:  csbhypf  3919  csbiebt  3920  cbvrabcsfw  3934  cbvralcsf  3935  cbvreucsf  3937  cbvrabcsf  3938  rspc2vd  3941  sbcnestgfw  4414  sbcnestgf  4419  csbnest1g  4425  csbun  4434  csbin  4435  csbdif  4523  csbif  4581  disjors  5123  invdisjrabw  5127  invdisjrab  5128  disjxiun  5139  disjxun  5140  sbcbr123  5196  eusvnf  5386  reusv2lem4  5395  reusv2  5397  moop2  5498  iunopeqop  5517  pofun  5602  opeliunxp  5739  elrnmpt1  5954  resmptf  6037  csbima12  6076  csbcog  6295  fvmpt2f  7000  fvmpts  7002  fvmptdf  7005  fvmpt2i  7009  fvmptex  7013  fmptco  7132  fmptcof  7133  fmptcos  7134  elabrex  7246  elabrexg  7247  fliftfuns  7316  csbov123  7456  ovmpos  7563  fvmpopr2d  7577  ofmpteq  7701  mpomptsx  8062  dmmpossx  8064  fmpox  8065  el2mpocsbcl  8084  offval22  8087  ovmptss  8092  fmpoco  8094  dfmpo  8101  mpoxeldm  8210  mpocurryd  8268  mpocurryvald  8269  fvmpocurryd  8270  eqerlem  8752  qliftfuns  8816  mptelixpg  8947  boxcutc  8953  xpf1o  9157  iunfi  9358  wdom2d  9597  ixpiunwdom  9607  hsmexlem2  10444  ac6c4  10498  iundom2g  10557  seqof2  14051  rlimcld2  15548  nfsum1  15662  sumeq2ii  15665  summolem3  15686  summolem2a  15687  zsum  15690  fsum  15692  sumss2  15698  fsumcvg2  15699  fsumclf  15710  fsumzcl2  15711  fsumsplitf  15714  sumsnf  15715  sumsns  15722  fsummsnunz  15726  fsumsplitsnun  15727  fsum2dlem  15742  fsumcom2  15746  fsumshftm  15753  fsum0diag2  15755  fsum00  15770  fsumabs  15773  fsumrlim  15783  fsumo1  15784  o1fsum  15785  fsumiun  15793  infcvgaux1i  15829  nfcprod1  15880  prodeq2ii  15883  prodmolem3  15903  prodmolem2a  15904  zprod  15907  fprod  15911  fprodntriv  15912  prodss  15917  fprodser  15919  fprodcllemf  15928  prodsn  15932  prodsnf  15934  fprodm1s  15940  fprodp1s  15941  prodsns  15942  fprodabs  15944  fprodn0  15949  fprod2dlem  15950  fprodcom2  15954  fproddivf  15957  fprodsplitf  15958  fprodsplit1f  15960  fprodle  15966  fprodmodd  15967  fprodefsum  16065  sumeven  16357  sumodd  16358  pcmpt  16854  pcmptdvds  16856  natpropd  17961  fucpropd  17962  gsummpt1n0  19913  gsumcom2  19923  gsummptnn0fz  19934  dprd2d2  19994  psrass1lemOLD  21867  psrass1lem  21870  mpfrcl  22024  coe1fzgsumdlem  22215  gsummoncoe1  22220  gsumply1eq  22221  evl1gsumdlem  22268  mdetralt2  22504  mdetunilem2  22508  madugsum  22538  fiuncmp  23301  ptcld  23510  ptcldmpt  23511  ptclsg  23512  elmptrab  23724  prdsdsf  24266  prdsxmet  24268  fsumcn  24781  fsum2cn  24782  ovolfiniun  25423  ovoliunlem3  25426  ovoliun  25427  ovoliun2  25428  ovoliunnul  25429  finiunmbl  25466  volfiniun  25469  iundisj  25470  iundisj2  25471  iunmbl  25475  iunmbl2  25479  itgss3  25737  itgfsum  25749  itgabs  25757  limciun  25816  dvmptfsum  25900  dvfsumle  25947  dvfsumleOLD  25948  dvfsumabs  25950  dvfsumlem1  25953  dvfsumlem2  25954  dvfsumlem2OLD  25955  dvfsumlem3  25956  dvfsumlem4  25957  dvfsumrlim  25959  dvfsumrlim2  25960  dvfsum2  25962  itgsubstlem  25976  itgsubst  25977  rlimcnp2  26891  fsumdvdscom  27110  fsumdvdsmul  27120  fsumdvdsmulOLD  27122  fsumvma  27139  dchrisumlema  27414  dchrisumlem2  27416  dchrisumlem3  27417  disjorsf  32363  disjabrex  32365  disjabrexf  32366  iundisjf  32372  iundisj2f  32373  disjunsn  32377  suppss2f  32417  2ndresdju  32428  fmptdF  32435  fmptcof2  32436  acunirnmpt2f  32440  aciunf1lem  32441  funcnv4mpt  32448  f1od2  32497  iundisjfi  32558  iundisj2fi  32559  fsumiunle  32586  gsummpt2co  32756  gsumpart  32763  gsumvsca1  32927  gsumvsca2  32928  rmfsupp2  32940  esumpfinvalf  33689  esum2dlem  33705  esumiun  33707  fiunelros  33787  measiun  33831  voliune  33842  volfiniune  33843  sbcaltop  35571  bj-sbeqALT  36372  phpreu  37071  finixpnum  37072  ptrest  37086  poimirlem23  37110  poimirlem24  37111  poimirlem25  37112  poimirlem26  37113  poimirlem27  37114  poimirlem28  37115  mbfposadd  37134  itgabsnc  37156  ftc1cnnclem  37158  ftc2nc  37169  fsumshftd  38418  riotasv2s  38424  cdleme31sn  39847  cdleme31sn1  39848  cdleme31se2  39850  cdleme32fva  39904  cdleme42b  39945  hlhilset  41401  evl1gprodd  41582  idomnnzgmulnz  41598  deg1gprod  41606  fmpocos  41719  mzpsubst  42162  rabdiophlem2  42216  elnn0rabdioph  42217  dvdsrabdioph  42224  fphpd  42230  monotuz  42356  oddcomabszz  42359  wdom2d2  42450  aomclem6  42477  flcidc  42592  fsumcnf  44377  sumsnd  44382  fiiuncl  44423  eliin2f  44464  disjf1  44550  disjrnmpt2  44555  disjinfi  44559  fmptf  44608  fmptff  44640  iuneqfzuzlem  44710  supxrleubrnmptf  44827  fsummulc1f  44953  fsumnncl  44954  fsumf1of  44956  fsumiunss  44957  fsumreclf  44958  fsumlessf  44959  fprodexp  44976  fprodabs2  44977  mccllem  44979  fprodcnlem  44981  fprodcn  44982  climeldmeqmpt  45050  climeldmeqmpt3  45071  climinf2mpt  45096  climinfmpt  45097  limsupequzmptf  45113  fprodcncf  45282  dvmptmulf  45319  dvnmptdivc  45320  dvmptfprod  45327  iblsplitf  45352  fourierdlem86  45574  fourierdlem112  45600  sge0iunmptlemfi  45795  sge0iunmptlemre  45797  sge0iunmpt  45800  sge0ltfirpmpt2  45808  sge0isummpt2  45814  sge0xaddlem2  45816  sge0xadd  45817  hoimbl2  46047  vonn0ioo2  46072  vonn0icc2  46074  csbafv12g  46511  csbaovg  46554  csbafv212g  46593  fsummsndifre  46706  fsumsplitsndif  46707  fsummmodsndifre  46708  fsummmodsnunz  46709  opeliun2xp  47390  dmmpossx2  47394