Theorem nfcsb1v 3919

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

Syntax hints:  Ⅎwnfc 2884  ⦋csb 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-sbc 3779  df-csb 3895

This theorem is referenced by:  csbhypf  3923  csbiebt  3924  cbvrabcsfw  3938  cbvralcsf  3939  cbvreucsf  3941  cbvrabcsf  3942  rspc2vd  3945  sbcnestgfw  4419  sbcnestgf  4424  csbnest1g  4430  csbun  4439  csbin  4440  csbdif  4528  csbif  4586  disjors  5130  invdisjrabw  5134  invdisjrab  5135  disjxiun  5146  disjxun  5147  sbcbr123  5203  eusvnf  5391  reusv2lem4  5400  reusv2  5402  moop2  5503  iunopeqop  5522  pofun  5607  opeliunxp  5744  elrnmpt1  5958  resmptf  6040  csbima12  6079  csbcog  6297  fvmpt2f  7000  fvmpts  7002  fvmptdf  7005  fvmpt2i  7009  fvmptex  7013  fmptco  7127  fmptcof  7128  fmptcos  7129  elabrex  7242  fliftfuns  7311  csbov123  7451  ovmpos  7556  fvmpopr2d  7569  ofmpteq  7692  mpomptsx  8050  dmmpossx  8052  fmpox  8053  el2mpocsbcl  8071  offval22  8074  ovmptss  8079  fmpoco  8081  dfmpo  8088  mpoxeldm  8196  mpocurryd  8254  mpocurryvald  8255  fvmpocurryd  8256  eqerlem  8737  qliftfuns  8798  mptelixpg  8929  boxcutc  8935  xpf1o  9139  iunfi  9340  wdom2d  9575  ixpiunwdom  9585  hsmexlem2  10422  ac6c4  10476  iundom2g  10535  seqof2  14026  rlimcld2  15522  nfsum1  15636  sumeq2ii  15639  summolem3  15660  summolem2a  15661  zsum  15664  fsum  15666  sumss2  15672  fsumcvg2  15673  fsumclf  15684  fsumzcl2  15685  fsumsplitf  15688  sumsnf  15689  sumsns  15696  fsummsnunz  15700  fsumsplitsnun  15701  fsum2dlem  15716  fsumcom2  15720  fsumshftm  15727  fsum0diag2  15729  fsum00  15744  fsumabs  15747  fsumrlim  15757  fsumo1  15758  o1fsum  15759  fsumiun  15767  infcvgaux1i  15803  nfcprod1  15854  prodeq2ii  15857  prodmolem3  15877  prodmolem2a  15878  zprod  15881  fprod  15885  fprodntriv  15886  prodss  15891  fprodser  15893  fprodcllemf  15902  prodsn  15906  prodsnf  15908  fprodm1s  15914  fprodp1s  15915  prodsns  15916  fprodabs  15918  fprodn0  15923  fprod2dlem  15924  fprodcom2  15928  fproddivf  15931  fprodsplitf  15932  fprodsplit1f  15934  fprodle  15940  fprodmodd  15941  fprodefsum  16038  sumeven  16330  sumodd  16331  pcmpt  16825  pcmptdvds  16827  natpropd  17929  fucpropd  17930  gsummpt1n0  19833  gsumcom2  19843  gsummptnn0fz  19854  dprd2d2  19914  psrass1lemOLD  21493  psrass1lem  21496  mpfrcl  21648  coe1fzgsumdlem  21825  gsummoncoe1  21828  gsumply1eq  21829  evl1gsumdlem  21875  mdetralt2  22111  mdetunilem2  22115  madugsum  22145  fiuncmp  22908  ptcld  23117  ptcldmpt  23118  ptclsg  23119  elmptrab  23331  prdsdsf  23873  prdsxmet  23875  fsumcn  24386  fsum2cn  24387  ovolfiniun  25018  ovoliunlem3  25021  ovoliun  25022  ovoliun2  25023  ovoliunnul  25024  finiunmbl  25061  volfiniun  25064  iundisj  25065  iundisj2  25066  iunmbl  25070  iunmbl2  25074  itgss3  25332  itgfsum  25344  itgabs  25352  limciun  25411  dvmptfsum  25492  dvfsumle  25538  dvfsumabs  25540  dvfsumlem1  25543  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsumrlim  25548  dvfsumrlim2  25549  dvfsum2  25551  itgsubstlem  25565  itgsubst  25566  rlimcnp2  26471  fsumdvdscom  26689  fsumdvdsmul  26699  fsumvma  26716  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  disjorsf  31842  disjabrex  31844  disjabrexf  31845  iundisjf  31851  iundisj2f  31852  disjunsn  31856  suppss2f  31894  2ndresdju  31905  fmptdF  31912  fmptcof2  31913  acunirnmpt2f  31917  aciunf1lem  31918  funcnv4mpt  31925  f1od2  31977  iundisjfi  32038  iundisj2fi  32039  fsumiunle  32066  gsummpt2co  32231  gsumpart  32238  gsumvsca1  32402  gsumvsca2  32403  rmfsupp2  32418  esumpfinvalf  33105  esum2dlem  33121  esumiun  33123  fiunelros  33203  measiun  33247  voliune  33258  volfiniune  33259  sbcaltop  34984  gg-dvfsumle  35213  gg-dvfsumlem2  35214  bj-sbeqALT  35828  phpreu  36520  finixpnum  36521  ptrest  36535  poimirlem23  36559  poimirlem24  36560  poimirlem25  36561  poimirlem26  36562  poimirlem27  36563  poimirlem28  36564  mbfposadd  36583  itgabsnc  36605  ftc1cnnclem  36607  ftc2nc  36618  fsumshftd  37870  riotasv2s  37876  cdleme31sn  39299  cdleme31sn1  39300  cdleme31se2  39302  cdleme32fva  39356  cdleme42b  39397  hlhilset  40853  fmpocos  41104  mzpsubst  41534  rabdiophlem2  41588  elnn0rabdioph  41589  dvdsrabdioph  41596  fphpd  41602  monotuz  41728  oddcomabszz  41731  wdom2d2  41822  aomclem6  41849  flcidc  41964  fsumcnf  43753  sumsnd  43758  elabrexg  43776  fiiuncl  43800  eliin2f  43841  disjf1  43928  disjrnmpt2  43934  disjinfi  43939  fmptf  43990  fmptff  44022  iuneqfzuzlem  44092  supxrleubrnmptf  44209  fsummulc1f  44335  fsumnncl  44336  fsumf1of  44338  fsumiunss  44339  fsumreclf  44340  fsumlessf  44341  fprodexp  44358  fprodabs2  44359  mccllem  44361  fprodcnlem  44363  fprodcn  44364  climeldmeqmpt  44432  climeldmeqmpt3  44453  climinf2mpt  44478  climinfmpt  44479  limsupequzmptf  44495  fprodcncf  44664  dvmptmulf  44701  dvnmptdivc  44702  dvmptfprod  44709  iblsplitf  44734  fourierdlem86  44956  fourierdlem112  44982  sge0iunmptlemfi  45177  sge0iunmptlemre  45179  sge0iunmpt  45182  sge0ltfirpmpt2  45190  sge0isummpt2  45196  sge0xaddlem2  45198  sge0xadd  45199  hoimbl2  45429  vonn0ioo2  45454  vonn0icc2  45456  csbafv12g  45893  csbaovg  45936  csbafv212g  45975  fsummsndifre  46088  fsumsplitsndif  46089  fsummmodsndifre  46090  fsummmodsnunz  46091  opeliun2xp  47056  dmmpossx2  47060