Theorem nfcsb1v 3909

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

Syntax hints:  Ⅎwnfc 2963  ⦋csb 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-sbc 3775  df-csb 3886

This theorem is referenced by:  csbhypf  3913  csbiebt  3914  cbvrabcsfw  3926  cbvralcsf  3927  cbvreucsf  3929  cbvrabcsf  3930  rspc2vd  3934  sbcnestgfw  4372  sbcnestgf  4377  csbnest1g  4383  csbun  4392  csbin  4393  csbif  4524  disjors  5049  invdisjrabw  5053  invdisjrab  5054  disjxiun  5065  disjxun  5066  sbcbr123  5122  eusvnf  5295  reusv2lem4  5304  reusv2  5306  moop2  5394  iunopeqop  5413  pofun  5493  opeliunxp  5621  elrnmpt1  5832  resmptf  5909  csbima12  5949  fvmpt2f  6771  fvmpts  6773  fvmptdf  6776  fvmpt2i  6780  fvmptex  6784  fmptco  6893  fmptcof  6894  fmptcos  6895  elabrex  7004  fliftfuns  7069  csbov123  7200  ovmpos  7300  ofmpteq  7430  mpomptsx  7764  dmmpossx  7766  fmpox  7767  el2mpocsbcl  7782  offval22  7785  ovmptss  7790  fmpoco  7792  dfmpo  7799  mpoxeldm  7879  mpocurryd  7937  mpocurryvald  7938  fvmpocurryd  7939  eqerlem  8325  qliftfuns  8386  mptelixpg  8501  boxcutc  8507  xpf1o  8681  iunfi  8814  wdom2d  9046  ixpiunwdom  9057  hsmexlem2  9851  ac6c4  9905  iundom2g  9964  seqof2  13431  rlimcld2  14937  nfsum1  15048  sumeq2ii  15052  summolem3  15073  summolem2a  15074  zsum  15077  fsum  15079  sumss2  15085  fsumcvg2  15086  fsumzcl2  15097  fsumsplitf  15100  sumsnf  15101  sumsns  15107  fsummsnunz  15111  fsumsplitsnun  15112  fsum2dlem  15127  fsumcom2  15131  fsumshftm  15138  fsum0diag2  15140  fsum00  15155  fsumabs  15158  fsumrlim  15168  fsumo1  15169  o1fsum  15170  fsumiun  15178  infcvgaux1i  15214  nfcprod1  15266  prodeq2ii  15269  prodmolem3  15289  prodmolem2a  15290  zprod  15293  fprod  15297  fprodntriv  15298  prodss  15303  fprodser  15305  fprodcllemf  15314  prodsn  15318  prodsnf  15320  fprodm1s  15326  fprodp1s  15327  prodsns  15328  fprodabs  15330  fprodn0  15335  fprod2dlem  15336  fprodcom2  15340  fproddivf  15343  fprodsplitf  15344  fprodsplit1f  15346  fprodle  15352  fprodmodd  15353  fprodefsum  15450  sumeven  15740  sumodd  15741  pcmpt  16230  pcmptdvds  16232  natpropd  17248  fucpropd  17249  gsummpt1n0  19087  gsumcom2  19097  gsummptnn0fz  19108  dprd2d2  19168  psrass1lem  20159  mpfrcl  20300  coe1fzgsumdlem  20471  gsummoncoe1  20474  gsumply1eq  20475  evl1gsumdlem  20521  mdetralt2  21220  mdetunilem2  21224  madugsum  21254  fiuncmp  22014  ptcld  22223  ptcldmpt  22224  ptclsg  22225  elmptrab  22437  prdsdsf  22979  prdsxmet  22981  fsumcn  23480  fsum2cn  23481  ovolfiniun  24104  ovoliunlem3  24107  ovoliun  24108  ovoliun2  24109  ovoliunnul  24110  finiunmbl  24147  volfiniun  24150  iundisj  24151  iundisj2  24152  iunmbl  24156  iunmbl2  24160  itgss3  24417  itgfsum  24429  itgabs  24437  limciun  24494  dvmptfsum  24574  dvfsumle  24620  dvfsumabs  24622  dvfsumlem1  24625  dvfsumlem2  24626  dvfsumlem3  24627  dvfsumlem4  24628  dvfsumrlim  24630  dvfsumrlim2  24631  dvfsum2  24633  itgsubstlem  24647  itgsubst  24648  rlimcnp2  25546  fsumdvdscom  25764  fsumdvdsmul  25774  fsumvma  25791  dchrisumlema  26066  dchrisumlem2  26068  dchrisumlem3  26069  disjorsf  30332  disjabrex  30334  disjabrexf  30335  iundisjf  30341  iundisj2f  30342  disjunsn  30346  suppss2f  30386  fmptdF  30403  fmptcof2  30404  acunirnmpt2f  30408  aciunf1lem  30409  funcnv4mpt  30416  f1od2  30459  iundisjfi  30521  iundisj2fi  30522  fsumiunle  30547  gsummpt2co  30688  gsumvsca1  30856  gsumvsca2  30857  rmfsupp2  30868  esumpfinvalf  31337  esum2dlem  31353  esumiun  31355  fiunelros  31435  measiun  31479  voliune  31490  volfiniune  31491  sbcaltop  33444  bj-sbeqALT  34219  csbdif  34608  phpreu  34878  finixpnum  34879  ptrest  34893  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  poimirlem28  34922  mbfposadd  34941  itgabsnc  34963  ftc1cnnclem  34967  ftc2nc  34978  fsumshftd  36090  riotasv2s  36096  cdleme31sn  37518  cdleme31sn1  37519  cdleme31se2  37521  cdleme32fva  37575  cdleme42b  37616  hlhilset  39072  mzpsubst  39352  rabdiophlem2  39406  elnn0rabdioph  39407  dvdsrabdioph  39414  fphpd  39420  monotuz  39545  oddcomabszz  39548  wdom2d2  39639  aomclem6  39666  flcidc  39781  csbcog  40001  fsumcnf  41285  sumsnd  41290  elabrexg  41310  fiiuncl  41334  eliin2f  41377  disjf1  41450  disjrnmpt2  41456  disjinfi  41461  fmptf  41516  iuneqfzuzlem  41609  supxrleubrnmptf  41734  fsumclf  41857  fsummulc1f  41858  fsumnncl  41859  fsumf1of  41862  fsumiunss  41863  fsumreclf  41864  fsumlessf  41865  fprodexp  41882  fprodabs2  41883  mccllem  41885  fprodcnlem  41887  fprodcn  41888  climeldmeqmpt  41956  climeldmeqmpt3  41977  climinf2mpt  42002  climinfmpt  42003  limsupequzmptf  42019  fprodcncf  42191  dvmptmulf  42229  dvnmptdivc  42230  dvmptfprod  42237  iblsplitf  42262  fourierdlem86  42484  fourierdlem112  42510  sge0iunmptlemfi  42702  sge0iunmptlemre  42704  sge0iunmpt  42707  sge0ltfirpmpt2  42715  sge0isummpt2  42721  sge0xaddlem2  42723  sge0xadd  42724  hoimbl2  42954  vonn0ioo2  42979  vonn0icc2  42981  csbafv12g  43343  csbaovg  43386  csbafv212g  43425  fsummsndifre  43539  fsumsplitsndif  43540  fsummmodsndifre  43541  fsummmodsnunz  43542  opeliun2xp  44388  dmmpossx2  44392