Theorem nfcsb1v 3886

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

Syntax hints:  Ⅎwnfc 2876  ⦋csb 3862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-sbc 3754  df-csb 3863

This theorem is referenced by:  csbhypf  3890  csbiebt  3891  cbvrabcsfw  3903  cbvralcsf  3904  cbvreucsf  3906  cbvrabcsf  3907  rspc2vd  3910  sbcnestgfw  4384  sbcnestgf  4389  csbnest1g  4395  csbun  4404  csbin  4405  csbdif  4487  csbif  4546  disjors  5090  invdisjrab  5094  disjxiun  5104  disjxun  5105  sbcbr123  5161  eusvnf  5347  reusv2lem4  5356  reusv2  5358  moop2  5462  iunopeqop  5481  pofun  5564  opeliunxp  5705  opeliun2xp  5706  elrnmpt1  5924  resmptf  6010  csbima12  6050  csbcog  6270  fvmpt2f  6969  fvmpts  6971  fvmptdf  6974  fvmpt2i  6978  fvmptex  6982  fmptco  7101  fmptcof  7102  fmptcos  7103  elabrex  7216  elabrexg  7217  fliftfuns  7289  csbov123  7431  ovmpos  7537  fvmpopr2d  7551  ofmpteq  7676  mpomptsx  8043  dmmpossx  8045  fmpox  8046  el2mpocsbcl  8064  offval22  8067  ovmptss  8072  fmpoco  8074  dfmpo  8081  mpoxeldm  8190  mpocurryd  8248  mpocurryvald  8249  fvmpocurryd  8250  eqerlem  8706  qliftfuns  8777  mptelixpg  8908  boxcutc  8914  xpf1o  9103  iunfi  9294  wdom2d  9533  ixpiunwdom  9543  hsmexlem2  10380  ac6c4  10434  iundom2g  10493  seqof2  14025  rlimcld2  15544  nfsum1  15656  sumeq2ii  15659  summolem3  15680  summolem2a  15681  zsum  15684  fsum  15686  sumss2  15692  fsumcvg2  15693  fsumclf  15704  fsumzcl2  15705  fsumsplitf  15708  sumsnf  15709  sumsns  15716  fsummsnunz  15720  fsumsplitsnun  15721  fsum2dlem  15736  fsumcom2  15740  fsumshftm  15747  fsum0diag2  15749  fsum00  15764  fsumabs  15767  fsumrlim  15777  fsumo1  15778  o1fsum  15779  fsumiun  15787  infcvgaux1i  15823  nfcprod1  15874  prodeq2ii  15877  prodmolem3  15899  prodmolem2a  15900  zprod  15903  fprod  15907  fprodntriv  15908  prodss  15913  fprodser  15915  fprodcllemf  15924  prodsn  15928  prodsnf  15930  fprodm1s  15936  fprodp1s  15937  prodsns  15938  fprodabs  15940  fprodn0  15945  fprod2dlem  15946  fprodcom2  15950  fproddivf  15953  fprodsplitf  15954  fprodsplit1f  15956  fprodle  15962  fprodmodd  15963  fprodefsum  16061  sumeven  16357  sumodd  16358  pcmpt  16863  pcmptdvds  16865  natpropd  17941  fucpropd  17942  gsummpt1n0  19895  gsumcom2  19905  gsummptnn0fz  19916  dprd2d2  19976  psrass1lem  21841  mpfrcl  21992  coe1fzgsumdlem  22190  gsummoncoe1  22195  gsumply1eq  22196  evl1gsumdlem  22243  mdetralt2  22496  mdetunilem2  22500  madugsum  22530  fiuncmp  23291  ptcld  23500  ptcldmpt  23501  ptclsg  23502  elmptrab  23714  prdsdsf  24255  prdsxmet  24257  fsumcn  24761  fsum2cn  24762  ovolfiniun  25402  ovoliunlem3  25405  ovoliun  25406  ovoliun2  25407  ovoliunnul  25408  finiunmbl  25445  volfiniun  25448  iundisj  25449  iundisj2  25450  iunmbl  25454  iunmbl2  25458  itgss3  25716  itgfsum  25728  itgabs  25736  limciun  25795  dvmptfsum  25879  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsumrlim  25938  dvfsumrlim2  25939  dvfsum2  25941  itgsubstlem  25955  itgsubst  25956  rlimcnp2  26876  fsumdvdscom  27095  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  fsumvma  27124  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  iunxpssiun1  32497  disjorsf  32509  disjabrex  32511  disjabrexf  32512  iundisjf  32518  iundisj2f  32519  disjunsn  32523  suppss2f  32562  2ndresdju  32573  fmptdF  32580  fmptcof2  32581  acunirnmpt2f  32585  aciunf1lem  32586  funcnv4mpt  32593  f1od2  32644  iundisjfi  32719  iundisj2fi  32720  fsumiunle  32754  gsummpt2co  32988  gsumpart  32997  gsumvsca1  33179  gsumvsca2  33180  rmfsupp2  33189  esumpfinvalf  34066  esum2dlem  34082  esumiun  34084  fiunelros  34164  measiun  34208  voliune  34219  volfiniune  34220  sbcaltop  35969  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  bj-sbeqALT  36888  phpreu  37598  finixpnum  37599  ptrest  37613  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  mbfposadd  37661  itgabsnc  37683  ftc1cnnclem  37685  ftc2nc  37696  fsumshftd  38945  riotasv2s  38951  cdleme31sn  40374  cdleme31sn1  40375  cdleme31se2  40377  cdleme32fva  40431  cdleme42b  40472  hlhilset  41928  evl1gprodd  42105  idomnnzgmulnz  42121  deg1gprod  42128  fmpocos  42222  mzpsubst  42736  rabdiophlem2  42790  elnn0rabdioph  42791  dvdsrabdioph  42798  fphpd  42804  monotuz  42930  oddcomabszz  42933  wdom2d2  43024  aomclem6  43048  flcidc  43159  fsumcnf  45015  sumsnd  45020  fiiuncl  45059  eliin2f  45098  disjf1  45177  disjrnmpt2  45182  disjinfi  45186  fmptf  45233  fmptff  45263  iuneqfzuzlem  45330  supxrleubrnmptf  45447  fsummulc1f  45569  fsumnncl  45570  fsumf1of  45572  fsumiunss  45573  fsumreclf  45574  fsumlessf  45575  fprodexp  45592  fprodabs2  45593  mccllem  45595  fprodcnlem  45597  fprodcn  45598  climeldmeqmpt  45666  climeldmeqmpt3  45687  climinf2mpt  45712  climinfmpt  45713  limsupequzmptf  45729  fprodcncf  45898  dvmptmulf  45935  dvnmptdivc  45936  dvmptfprod  45943  iblsplitf  45968  fourierdlem86  46190  fourierdlem112  46216  sge0f1o  46380  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0ltfirpmpt2  46424  sge0isummpt2  46430  sge0xaddlem2  46432  sge0xadd  46433  hoimbl2  46663  vonn0ioo2  46688  vonn0icc2  46690  csbafv12g  47138  csbaovg  47181  csbafv212g  47220  fsummsndifre  47373  fsumsplitsndif  47374  fsummmodsndifre  47375  fsummmodsnunz  47376  dmmpossx2  48325