Theorem nfcsb1v 3862

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

Syntax hints:  Ⅎwnfc 2887  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-sbc 3731  df-csb 3839

This theorem is referenced by:  csbhypf  3866  csbiebt  3867  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  rspc2vd  3886  sbcnestgfw  4356  sbcnestgf  4361  csbnest1g  4367  csbun  4376  csbin  4377  csbdif  4460  csbif  4519  disjors  5062  invdisjrab  5066  disjxiun  5076  disjxun  5077  sbcbr123  5133  eusvnf  5328  reusv2lem4  5337  reusv2  5339  moop2  5450  iunopeqop  5469  iunopeqopOLD  5470  pofun  5551  opeliunxp  5692  opeliun2xp  5693  elrnmpt1  5909  resmptf  5998  csbima12  6038  csbcog  6255  fvmpt2f  6943  fvmpts  6946  fvmptdf  6949  fvmpt2i  6953  fvmptex  6957  fmptco  7078  fmptcof  7079  fmptcos  7080  elabrex  7193  elabrexg  7194  fliftfuns  7265  csbov123  7407  ovmpos  7511  fvmpopr2d  7525  ofmpteq  7650  mpomptsx  8013  dmmpossx  8015  fmpox  8016  el2mpocsbcl  8031  offval22  8034  ovmptss  8039  fmpoco  8041  dfmpo  8048  mpoxeldm  8158  mpocurryd  8216  mpocurryvald  8217  fvmpocurryd  8218  eqerlem  8676  qliftfuns  8748  mptelixpg  8880  boxcutc  8886  xpf1o  9074  iunfi  9250  wdom2d  9492  ixpiunwdom  9502  hsmexlem2  10347  ac6c4  10401  iundom2g  10460  seqof2  14020  rlimcld2  15538  nfsum1  15650  sumeq2ii  15653  summolem3  15674  summolem2a  15675  zsum  15678  fsum  15680  sumss2  15686  fsumcvg2  15687  fsumclf  15698  fsumzcl2  15699  fsumsplitf  15702  sumsnf  15703  sumsns  15710  fsummsnunz  15714  fsumsplitsnun  15715  fsum2dlem  15730  fsumcom2  15734  fsumshftm  15741  fsum0diag2  15743  fsum00  15759  fsumabs  15762  fsumrlim  15772  fsumo1  15773  o1fsum  15774  fsumiun  15782  infcvgaux1i  15820  nfcprod1  15871  prodeq2ii  15874  prodmolem3  15896  prodmolem2a  15897  zprod  15900  fprod  15904  fprodntriv  15905  prodss  15910  fprodser  15912  fprodcllemf  15921  prodsn  15925  prodsnf  15927  fprodm1s  15933  fprodp1s  15934  prodsns  15935  fprodabs  15937  fprodn0  15942  fprod2dlem  15943  fprodcom2  15947  fproddivf  15950  fprodsplitf  15951  fprodsplit1f  15953  fprodle  15959  fprodmodd  15960  fprodefsum  16058  sumeven  16354  sumodd  16355  pcmpt  16861  pcmptdvds  16863  natpropd  17944  fucpropd  17945  gsummpt1n0  19938  gsumcom2  19948  gsummptnn0fz  19959  dprd2d2  20019  psrass1lem  21915  mpfrcl  22068  coe1fzgsumdlem  22296  gsummoncoe1  22301  gsumply1eq  22302  evl1gsumdlem  22349  mdetralt2  22599  mdetunilem2  22603  madugsum  22633  fiuncmp  23394  ptcld  23603  ptcldmpt  23604  ptclsg  23605  elmptrab  23817  prdsdsf  24357  prdsxmet  24359  fsumcn  24862  fsum2cn  24863  ovolfiniun  25493  ovoliunlem3  25496  ovoliun  25497  ovoliun2  25498  ovoliunnul  25499  finiunmbl  25536  volfiniun  25539  iundisj  25540  iundisj2  25541  iunmbl  25545  iunmbl2  25549  itgss3  25807  itgfsum  25819  itgabs  25827  limciun  25886  dvmptfsum  25967  dvfsumle  26013  dvfsumabs  26015  dvfsumlem1  26018  dvfsumlem2  26019  dvfsumlem3  26020  dvfsumlem4  26021  dvfsumrlim  26023  dvfsumrlim2  26024  dvfsum2  26026  itgsubstlem  26040  itgsubst  26041  rlimcnp2  26955  fsumdvdscom  27173  fsumdvdsmul  27183  fsumvma  27201  dchrisumlema  27476  dchrisumlem2  27478  dchrisumlem3  27479  iunxpssiun1  32664  disjorsf  32676  disjabrex  32678  disjabrexf  32679  iundisjf  32685  iundisj2f  32686  disjunsn  32690  suppss2f  32737  2ndresdju  32748  fmptdF  32755  fmptcof2  32756  acunirnmpt2f  32760  aciunf1lem  32761  funcnv4mpt  32767  f1od2  32818  iundisjfi  32895  iundisj2fi  32896  fsumiunle  32928  gsummpt2co  33136  gsummptp1  33145  gsumpart  33151  gsumvsca1  33314  gsumvsca2  33315  rmfsupp2  33326  esumpfinvalf  34267  esum2dlem  34283  esumiun  34285  fiunelros  34365  measiun  34409  voliune  34420  volfiniune  34421  sbcaltop  36216  weiunpo  36700  weiunso  36701  weiunfr  36702  weiunse  36703  csbttc  36744  bj-sbeqALT  37260  phpreu  37978  finixpnum  37979  ptrest  37993  poimirlem23  38017  poimirlem24  38018  poimirlem25  38019  poimirlem26  38020  poimirlem27  38021  poimirlem28  38022  mbfposadd  38041  itgabsnc  38063  ftc1cnnclem  38065  ftc2nc  38076  fsumshftd  39451  riotasv2s  39457  cdleme31sn  40879  cdleme31sn1  40880  cdleme31se2  40882  cdleme32fva  40936  cdleme42b  40977  hlhilset  42433  evl1gprodd  42609  idomnnzgmulnz  42625  deg1gprod  42632  fmpocos  42727  mzpsubst  43204  rabdiophlem2  43254  elnn0rabdioph  43255  dvdsrabdioph  43262  fphpd  43268  monotuz  43393  oddcomabszz  43396  wdom2d2  43487  aomclem6  43511  flcidc  43622  fsumcnf  45476  sumsnd  45481  fiiuncl  45520  eliin2f  45558  disjf1  45637  disjrnmpt2  45642  disjinfi  45646  fmptf  45690  fmptff  45720  iuneqfzuzlem  45786  supxrleubrnmptf  45901  fsummulc1f  46023  fsumnncl  46024  fsumf1of  46026  fsumiunss  46027  fsumreclf  46028  fsumlessf  46029  fprodexp  46046  fprodabs2  46047  mccllem  46049  fprodcnlem  46051  fprodcn  46052  climeldmeqmpt  46118  climeldmeqmpt3  46139  climinf2mpt  46164  climinfmpt  46165  limsupequzmptf  46181  fprodcncf  46350  dvmptmulf  46387  dvnmptdivc  46388  dvmptfprod  46395  iblsplitf  46420  fourierdlem86  46642  fourierdlem112  46668  sge0f1o  46832  sge0iunmptlemfi  46863  sge0iunmptlemre  46865  sge0iunmpt  46868  sge0ltfirpmpt2  46876  sge0isummpt2  46882  sge0xaddlem2  46884  sge0xadd  46885  hoimbl2  47115  vonn0ioo2  47140  vonn0icc2  47142  csbafv12g  47607  csbaovg  47650  csbafv212g  47689  fsummsndifre  47850  fsumsplitsndif  47851  fsummmodsndifre  47852  fsummmodsnunz  47853  dmmpossx2  48835