Theorem nfcsb1v 3880

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

This proof depends on syntax axioms:  Ⅎwnfc 2913  ⦋csb 3856

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-sbc 3748  df-csb 3857

This theorem is used by:  csbhypf  3884  csbiebt  3885  cbvrabcsfw  3897  cbvralcsf  3898  cbvreucsf  3900  cbvrabcsf  3901  rspc2vd  3904  sbcnestgfw  4389  sbcnestgf  4394  csbnest1g  4400  csbun  4409  csbin  4410  csbdif  4491  csbif  4550  disjors  5097  invdisjrab  5101  disjxiun  5111  disjxun  5112  sbcbr123  5170  eusvnf  5368  reusv2lem4  5377  reusv2  5379  moop2  5490  iunopeqop  5509  iunopeqopOLD  5510  pofun  5592  opeliunxp  5733  opeliun2xp  5734  elrnmpt1  5955  resmptf  6046  csbima12  6086  csbcog  6305  fvmpt2f  6997  fvmpts  7000  fvmptdf  7003  fvmpt2i  7007  fvmptex  7011  fmptco  7132  fmptcof  7133  fmptcos  7134  elabrex  7247  elabrexg  7248  fliftfuns  7323  csbov123  7467  ovmpos  7571  fvmpopr2d  7585  ofmpteq  7710  mpomptsx  8070  dmmpossx  8072  fmpox  8073  el2mpocsbcl  8089  offval22  8092  ovmptss  8097  fmpoco  8099  dfmpo  8106  mpoxeldm  8216  mpocurryd  8274  mpocurryvald  8275  fvmpocurryd  8276  eqerlem  8739  qliftfuns  8811  mptelixpg  8942  boxcutc  8948  xpf1o  9137  iunfi  9310  wdom2d  9552  ixpiunwdom  9562  hsmexlem2  10429  ac6c4  10483  iundom2g  10542  seqof2  14116  rlimcld2  15655  nfsum1  15767  sumeq2ii  15770  summolem3  15791  summolem2a  15792  zsum  15795  fsum  15797  sumss2  15803  fsumcvg2  15804  fsumclf  15815  fsumzcl2  15816  fsumsplitf  15819  sumsnf  15820  sumsns  15827  fsummsnunz  15831  fsumsplitsnun  15832  fsum2dlem  15847  fsumcom2  15851  fsumshftm  15858  fsum0diag2  15860  fsum00  15876  fsumabs  15879  fsumrlim  15889  fsumo1  15890  o1fsum  15891  fsumiun  15899  infcvgaux1i  15937  nfcprod1  15988  prodeq2ii  15991  prodmolem3  16013  prodmolem2a  16014  zprod  16017  fprod  16021  fprodntriv  16022  prodss  16027  fprodser  16029  fprodcllemf  16038  prodsn  16042  prodsnf  16044  fprodm1s  16050  fprodp1s  16051  prodsns  16052  fprodabs  16054  fprodn0  16059  fprod2dlem  16060  fprodcom2  16064  fproddivf  16067  fprodsplitf  16068  fprodsplit1f  16070  fprodle  16076  fprodmodd  16077  fprodefsum  16174  sumeven  16470  sumodd  16471  pcmpt  16977  pcmptdvds  16979  natpropd  18061  fucpropd  18062  gsummpt1n0  20066  gsumcom2  20076  gsummptnn0fz  20087  dprd2d2  20147  psrass1lem  22120  mpfrcl  22273  coe1fzgsumdlem  22500  gsummoncoe1  22505  gsumply1eq  22506  evl1gsumdlem  22553  mdetralt2  22803  mdetunilem2  22807  madugsum  22837  fiuncmp  23598  ptcld  23807  ptcldmpt  23808  ptclsg  23809  elmptrab  24021  prdsdsf  24561  prdsxmet  24563  fsumcn  25066  fsum2cn  25067  ovolfiniun  25697  ovoliunlem3  25700  ovoliun  25701  ovoliun2  25702  ovoliunnul  25703  finiunmbl  25740  volfiniun  25743  iundisj  25744  iundisj2  25745  iunmbl  25749  iunmbl2  25753  itgss3  26011  itgfsum  26023  itgabs  26031  limciun  26090  dvmptfsum  26171  dvfsumle  26217  dvfsumabs  26219  dvfsumlem1  26222  dvfsumlem2  26223  dvfsumlem3  26224  dvfsumlem4  26225  dvfsumrlim  26227  dvfsumrlim2  26228  dvfsum2  26230  itgsubstlem  26244  itgsubst  26245  rlimcnp2  27168  fsumdvdscom  27386  fsumdvdsmul  27396  fsumvma  27414  dchrisumlema  27689  dchrisumlem2  27691  dchrisumlem3  27692  iunxpssiun1  32950  disjorsf  32962  disjabrex  32964  disjabrexf  32965  iundisjf  32971  iundisj2f  32972  disjunsn  32976  suppss2f  33020  2ndresdju  33031  fmptdf2  33038  fmptcof2  33039  acunirnmpt2f  33043  aciunf1lem  33044  funcnv4mpt  33050  f1od2  33101  iundisjfi  33178  iundisj2fi  33179  fsumiunle  33210  gsummpt2co  33399  gsummptp1  33408  gsumpart  33414  gsumvsca1  33577  gsumvsca2  33578  rmfsupp2  33588  esumpfinvalf  34497  esum2dlem  34513  esumiun  34515  fiunelros  34596  measiun  34640  voliune  34651  volfiniune  34652  sbcaltop  36494  weiunpo  37017  weiunso  37018  weiunfr  37019  weiunse  37020  csbttc  37061  bj-sbeqALT  37576  phpreu  38296  finixpnum  38297  ptrest  38311  poimirlem23  38335  poimirlem24  38336  poimirlem25  38337  poimirlem26  38338  poimirlem27  38339  poimirlem28  38340  mbfposadd  38359  itgabsnc  38381  ftc1cnnclem  38383  ftc2nc  38394  fsumshftd  39767  riotasv2s  39773  cdleme31sn  41195  cdleme31sn1  41196  cdleme31se2  41198  cdleme32fva  41252  cdleme42b  41293  hlhilset  42749  evl1gprodd  42925  idomnnzgmulnz  42941  deg1gprod  42948  fmpocos  43045  mzpsubst  43520  rabdiophlem2  43570  elnn0rabdioph  43571  dvdsrabdioph  43578  fphpd  43584  monotuz  43709  oddcomabszz  43712  wdom2d2  43803  aomclem6  43827  flcidc  43938  fsumcnf  45782  sumsnd  45787  fiiuncl  45826  eliin2f  45863  disjf1  45942  disjrnmpt2  45947  disjinfi  45951  fmptf  45995  fmptff  46025  iuneqfzuzlem  46091  supxrleubrnmptf  46206  fsummulc1f  46328  fsumnncl  46329  fsumf1of  46331  fsumiunss  46332  fsumreclf  46333  fsumlessf  46334  fprodexp  46351  fprodabs2  46352  mccllem  46354  fprodcnlem  46356  fprodcn  46357  climeldmeqmpt  46423  climeldmeqmpt3  46444  climinf2mpt  46469  climinfmpt  46470  limsupequzmptf  46486  fprodcncf  46655  dvmptmulf  46692  dvnmptdivc  46693  dvmptfprod  46700  iblsplitf  46725  fourierdlem86  46947  fourierdlem112  46973  sge0f1o  47137  sge0iunmptlemfi  47168  sge0iunmptlemre  47170  sge0iunmpt  47173  sge0ltfirpmpt2  47181  sge0isummpt2  47187  sge0xaddlem2  47189  sge0xadd  47190  hoimbl2  47420  vonn0ioo2  47445  vonn0icc2  47447  csbafv12g  47915  csbaovg  47958  csbafv212g  47997  fsummsndifre  48158  fsumsplitsndif  48159  fsummmodsndifre  48160  fsummmodsnunz  48161  dmmpossx2  49158