Theorem nfcsb1v 3878

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

Syntax hints:  Ⅎwnfc 2910  ⦋csb 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-sbc 3746  df-csb 3855

This theorem is referenced by:  csbhypf  3882  csbiebt  3883  cbvrabcsfw  3895  cbvralcsf  3896  cbvreucsf  3898  cbvrabcsf  3899  rspc2vd  3902  sbcnestgfw  4387  sbcnestgf  4392  csbnest1g  4398  csbun  4407  csbin  4408  csbdif  4487  csbif  4546  disjors  5093  invdisjrab  5097  disjxiun  5107  disjxun  5108  sbcbr123  5166  eusvnf  5365  reusv2lem4  5374  reusv2  5376  moop2  5487  iunopeqop  5506  iunopeqopOLD  5507  pofun  5589  opeliunxp  5730  opeliun2xp  5731  elrnmpt1  5952  resmptf  6043  csbima12  6083  csbcog  6300  fvmpt2f  6992  fvmpts  6995  fvmptdf  6998  fvmpt2i  7002  fvmptex  7006  fmptco  7127  fmptcof  7128  fmptcos  7129  elabrex  7242  elabrexg  7243  fliftfuns  7314  csbov123  7456  ovmpos  7560  fvmpopr2d  7574  ofmpteq  7699  mpomptsx  8062  dmmpossx  8064  fmpox  8065  el2mpocsbcl  8081  offval22  8084  ovmptss  8089  fmpoco  8091  dfmpo  8098  mpoxeldm  8208  mpocurryd  8266  mpocurryvald  8267  fvmpocurryd  8268  eqerlem  8731  qliftfuns  8803  mptelixpg  8934  boxcutc  8940  xpf1o  9128  iunfi  9301  wdom2d  9543  ixpiunwdom  9553  hsmexlem2  10412  ac6c4  10466  iundom2g  10525  seqof2  14098  rlimcld2  15631  nfsum1  15743  sumeq2ii  15746  summolem3  15767  summolem2a  15768  zsum  15771  fsum  15773  sumss2  15779  fsumcvg2  15780  fsumclf  15791  fsumzcl2  15792  fsumsplitf  15795  sumsnf  15796  sumsns  15803  fsummsnunz  15807  fsumsplitsnun  15808  fsum2dlem  15823  fsumcom2  15827  fsumshftm  15834  fsum0diag2  15836  fsum00  15852  fsumabs  15855  fsumrlim  15865  fsumo1  15866  o1fsum  15867  fsumiun  15875  infcvgaux1i  15913  nfcprod1  15964  prodeq2ii  15967  prodmolem3  15989  prodmolem2a  15990  zprod  15993  fprod  15997  fprodntriv  15998  prodss  16003  fprodser  16005  fprodcllemf  16014  prodsn  16018  prodsnf  16020  fprodm1s  16026  fprodp1s  16027  prodsns  16028  fprodabs  16030  fprodn0  16035  fprod2dlem  16036  fprodcom2  16040  fproddivf  16043  fprodsplitf  16044  fprodsplit1f  16046  fprodle  16052  fprodmodd  16053  fprodefsum  16150  sumeven  16446  sumodd  16447  pcmpt  16953  pcmptdvds  16955  natpropd  18037  fucpropd  18038  gsummpt1n0  20036  gsumcom2  20046  gsummptnn0fz  20057  dprd2d2  20117  psrass1lem  22064  mpfrcl  22217  coe1fzgsumdlem  22444  gsummoncoe1  22449  gsumply1eq  22450  evl1gsumdlem  22497  mdetralt2  22747  mdetunilem2  22751  madugsum  22781  fiuncmp  23542  ptcld  23751  ptcldmpt  23752  ptclsg  23753  elmptrab  23965  prdsdsf  24505  prdsxmet  24507  fsumcn  25010  fsum2cn  25011  ovolfiniun  25641  ovoliunlem3  25644  ovoliun  25645  ovoliun2  25646  ovoliunnul  25647  finiunmbl  25684  volfiniun  25687  iundisj  25688  iundisj2  25689  iunmbl  25693  iunmbl2  25697  itgss3  25955  itgfsum  25967  itgabs  25975  limciun  26034  dvmptfsum  26115  dvfsumle  26161  dvfsumabs  26163  dvfsumlem1  26166  dvfsumlem2  26167  dvfsumlem3  26168  dvfsumlem4  26169  dvfsumrlim  26171  dvfsumrlim2  26172  dvfsum2  26174  itgsubstlem  26188  itgsubst  26189  rlimcnp2  27112  fsumdvdscom  27330  fsumdvdsmul  27340  fsumvma  27358  dchrisumlema  27633  dchrisumlem2  27635  dchrisumlem3  27636  iunxpssiun1  32894  disjorsf  32906  disjabrex  32908  disjabrexf  32909  iundisjf  32915  iundisj2f  32916  disjunsn  32920  suppss2f  32964  2ndresdju  32975  fmptdF  32982  fmptcof2  32983  acunirnmpt2f  32987  aciunf1lem  32988  funcnv4mpt  32994  f1od2  33045  iundisjfi  33122  iundisj2fi  33123  fsumiunle  33154  gsummpt2co  33349  gsummptp1  33358  gsumpart  33364  gsumvsca1  33527  gsumvsca2  33528  rmfsupp2  33538  esumpfinvalf  34447  esum2dlem  34463  esumiun  34465  fiunelros  34545  measiun  34589  voliune  34600  volfiniune  34601  sbcaltop  36454  weiunpo  36957  weiunso  36958  weiunfr  36959  weiunse  36960  csbttc  37001  bj-sbeqALT  37516  phpreu  38236  finixpnum  38237  ptrest  38251  poimirlem23  38275  poimirlem24  38276  poimirlem25  38277  poimirlem26  38278  poimirlem27  38279  poimirlem28  38280  mbfposadd  38299  itgabsnc  38321  ftc1cnnclem  38323  ftc2nc  38334  fsumshftd  39707  riotasv2s  39713  cdleme31sn  41135  cdleme31sn1  41136  cdleme31se2  41138  cdleme32fva  41192  cdleme42b  41233  hlhilset  42689  evl1gprodd  42865  idomnnzgmulnz  42881  deg1gprod  42888  fmpocos  42985  mzpsubst  43462  rabdiophlem2  43512  elnn0rabdioph  43513  dvdsrabdioph  43520  fphpd  43526  monotuz  43651  oddcomabszz  43654  wdom2d2  43745  aomclem6  43769  flcidc  43880  fsumcnf  45724  sumsnd  45729  fiiuncl  45768  eliin2f  45805  disjf1  45884  disjrnmpt2  45889  disjinfi  45893  fmptf  45937  fmptff  45967  iuneqfzuzlem  46033  supxrleubrnmptf  46148  fsummulc1f  46270  fsumnncl  46271  fsumf1of  46273  fsumiunss  46274  fsumreclf  46275  fsumlessf  46276  fprodexp  46293  fprodabs2  46294  mccllem  46296  fprodcnlem  46298  fprodcn  46299  climeldmeqmpt  46365  climeldmeqmpt3  46386  climinf2mpt  46411  climinfmpt  46412  limsupequzmptf  46428  fprodcncf  46597  dvmptmulf  46634  dvnmptdivc  46635  dvmptfprod  46642  iblsplitf  46667  fourierdlem86  46889  fourierdlem112  46915  sge0f1o  47079  sge0iunmptlemfi  47110  sge0iunmptlemre  47112  sge0iunmpt  47115  sge0ltfirpmpt2  47123  sge0isummpt2  47129  sge0xaddlem2  47131  sge0xadd  47132  hoimbl2  47362  vonn0ioo2  47387  vonn0icc2  47389  csbafv12g  47857  csbaovg  47900  csbafv212g  47939  fsummsndifre  48100  fsumsplitsndif  48101  fsummmodsndifre  48102  fsummmodsnunz  48103  dmmpossx2  49100