Theorem nfcsb1v 3879

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

Syntax hints:  Ⅎwnfc 2912  ⦋csb 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-sbc 3748  df-csb 3856

This theorem is referenced by:  csbhypf  3883  csbiebt  3884  cbvrabcsfw  3896  cbvralcsf  3897  cbvreucsf  3899  cbvrabcsf  3900  rspc2vd  3903  sbcnestgfw  4378  sbcnestgf  4383  csbnest1g  4389  csbun  4398  csbin  4399  csbdif  4482  csbif  4541  disjors  5087  invdisjrab  5091  disjxiun  5101  disjxun  5102  sbcbr123  5158  eusvnf  5353  reusv2lem4  5362  reusv2  5364  moop2  5475  iunopeqop  5494  iunopeqopOLD  5495  pofun  5577  opeliunxp  5718  opeliun2xp  5719  elrnmpt1  5940  resmptf  6031  csbima12  6071  csbcog  6287  fvmpt2f  6980  fvmpts  6983  fvmptdf  6986  fvmpt2i  6990  fvmptex  6994  fmptco  7115  fmptcof  7116  fmptcos  7117  elabrex  7230  elabrexg  7231  fliftfuns  7302  csbov123  7444  ovmpos  7548  fvmpopr2d  7562  ofmpteq  7687  mpomptsx  8049  dmmpossx  8051  fmpox  8052  el2mpocsbcl  8068  offval22  8071  ovmptss  8076  fmpoco  8078  dfmpo  8085  mpoxeldm  8195  mpocurryd  8253  mpocurryvald  8254  fvmpocurryd  8255  eqerlem  8718  qliftfuns  8790  mptelixpg  8921  boxcutc  8927  xpf1o  9115  iunfi  9288  wdom2d  9530  ixpiunwdom  9540  hsmexlem2  10399  ac6c4  10453  iundom2g  10512  seqof2  14084  rlimcld2  15617  nfsum1  15729  sumeq2ii  15732  summolem3  15753  summolem2a  15754  zsum  15757  fsum  15759  sumss2  15765  fsumcvg2  15766  fsumclf  15777  fsumzcl2  15778  fsumsplitf  15781  sumsnf  15782  sumsns  15789  fsummsnunz  15793  fsumsplitsnun  15794  fsum2dlem  15809  fsumcom2  15813  fsumshftm  15820  fsum0diag2  15822  fsum00  15838  fsumabs  15841  fsumrlim  15851  fsumo1  15852  o1fsum  15853  fsumiun  15861  infcvgaux1i  15899  nfcprod1  15950  prodeq2ii  15953  prodmolem3  15975  prodmolem2a  15976  zprod  15979  fprod  15983  fprodntriv  15984  prodss  15989  fprodser  15991  fprodcllemf  16000  prodsn  16004  prodsnf  16006  fprodm1s  16012  fprodp1s  16013  prodsns  16014  fprodabs  16016  fprodn0  16021  fprod2dlem  16022  fprodcom2  16026  fproddivf  16029  fprodsplitf  16030  fprodsplit1f  16032  fprodle  16038  fprodmodd  16039  fprodefsum  16137  sumeven  16433  sumodd  16434  pcmpt  16940  pcmptdvds  16942  natpropd  18024  fucpropd  18025  gsummpt1n0  20023  gsumcom2  20033  gsummptnn0fz  20044  dprd2d2  20104  psrass1lem  22040  mpfrcl  22193  coe1fzgsumdlem  22420  gsummoncoe1  22425  gsumply1eq  22426  evl1gsumdlem  22473  mdetralt2  22723  mdetunilem2  22727  madugsum  22757  fiuncmp  23518  ptcld  23727  ptcldmpt  23728  ptclsg  23729  elmptrab  23941  prdsdsf  24481  prdsxmet  24483  fsumcn  24986  fsum2cn  24987  ovolfiniun  25617  ovoliunlem3  25620  ovoliun  25621  ovoliun2  25622  ovoliunnul  25623  finiunmbl  25660  volfiniun  25663  iundisj  25664  iundisj2  25665  iunmbl  25669  iunmbl2  25673  itgss3  25931  itgfsum  25943  itgabs  25951  limciun  26010  dvmptfsum  26091  dvfsumle  26137  dvfsumabs  26139  dvfsumlem1  26142  dvfsumlem2  26143  dvfsumlem3  26144  dvfsumlem4  26145  dvfsumrlim  26147  dvfsumrlim2  26148  dvfsum2  26150  itgsubstlem  26164  itgsubst  26165  rlimcnp2  27085  fsumdvdscom  27303  fsumdvdsmul  27313  fsumvma  27331  dchrisumlema  27606  dchrisumlem2  27608  dchrisumlem3  27609  iunxpssiun1  32819  disjorsf  32831  disjabrex  32833  disjabrexf  32834  iundisjf  32840  iundisj2f  32841  disjunsn  32845  suppss2f  32891  2ndresdju  32902  fmptdF  32909  fmptcof2  32910  acunirnmpt2f  32914  aciunf1lem  32915  funcnv4mpt  32921  f1od2  32972  iundisjfi  33049  iundisj2fi  33050  fsumiunle  33081  gsummpt2co  33276  gsummptp1  33285  gsumpart  33291  gsumvsca1  33454  gsumvsca2  33455  rmfsupp2  33465  esumpfinvalf  34378  esum2dlem  34394  esumiun  34396  fiunelros  34476  measiun  34520  voliune  34531  volfiniune  34532  sbcaltop  36339  weiunpo  36833  weiunso  36834  weiunfr  36835  weiunse  36836  csbttc  36877  bj-sbeqALT  37392  phpreu  38110  finixpnum  38111  ptrest  38125  poimirlem23  38149  poimirlem24  38150  poimirlem25  38151  poimirlem26  38152  poimirlem27  38153  poimirlem28  38154  mbfposadd  38173  itgabsnc  38195  ftc1cnnclem  38197  ftc2nc  38208  fsumshftd  39583  riotasv2s  39589  cdleme31sn  41011  cdleme31sn1  41012  cdleme31se2  41014  cdleme32fva  41068  cdleme42b  41109  hlhilset  42565  evl1gprodd  42741  idomnnzgmulnz  42757  deg1gprod  42764  fmpocos  42859  mzpsubst  43336  rabdiophlem2  43386  elnn0rabdioph  43387  dvdsrabdioph  43394  fphpd  43400  monotuz  43525  oddcomabszz  43528  wdom2d2  43619  aomclem6  43643  flcidc  43754  fsumcnf  45600  sumsnd  45605  fiiuncl  45644  eliin2f  45681  disjf1  45760  disjrnmpt2  45765  disjinfi  45769  fmptf  45813  fmptff  45843  iuneqfzuzlem  45909  supxrleubrnmptf  46024  fsummulc1f  46146  fsumnncl  46147  fsumf1of  46149  fsumiunss  46150  fsumreclf  46151  fsumlessf  46152  fprodexp  46169  fprodabs2  46170  mccllem  46172  fprodcnlem  46174  fprodcn  46175  climeldmeqmpt  46241  climeldmeqmpt3  46262  climinf2mpt  46287  climinfmpt  46288  limsupequzmptf  46304  fprodcncf  46473  dvmptmulf  46510  dvnmptdivc  46511  dvmptfprod  46518  iblsplitf  46543  fourierdlem86  46765  fourierdlem112  46791  sge0f1o  46955  sge0iunmptlemfi  46986  sge0iunmptlemre  46988  sge0iunmpt  46991  sge0ltfirpmpt2  46999  sge0isummpt2  47005  sge0xaddlem2  47007  sge0xadd  47008  hoimbl2  47238  vonn0ioo2  47263  vonn0icc2  47265  csbafv12g  47730  csbaovg  47773  csbafv212g  47812  fsummsndifre  47973  fsumsplitsndif  47974  fsummmodsndifre  47975  fsummmodsnunz  47976  dmmpossx2  48969