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

Syntax hints:  Ⅎwnfc 2884  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbhypf  3866  csbiebt  3867  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  rspc2vd  3886  sbcnestgfw  4362  sbcnestgf  4367  csbnest1g  4373  csbun  4382  csbin  4383  csbdif  4466  csbif  4525  disjors  5069  invdisjrab  5073  disjxiun  5083  disjxun  5084  sbcbr123  5140  eusvnf  5329  reusv2lem4  5338  reusv2  5340  moop2  5450  iunopeqop  5469  pofun  5550  opeliunxp  5691  opeliun2xp  5692  elrnmpt1  5909  resmptf  5998  csbima12  6038  csbcog  6255  fvmpt2f  6942  fvmpts  6945  fvmptdf  6948  fvmpt2i  6952  fvmptex  6956  fmptco  7076  fmptcof  7077  fmptcos  7078  elabrex  7190  elabrexg  7191  fliftfuns  7262  csbov123  7404  ovmpos  7508  fvmpopr2d  7522  ofmpteq  7647  mpomptsx  8010  dmmpossx  8012  fmpox  8013  el2mpocsbcl  8028  offval22  8031  ovmptss  8036  fmpoco  8038  dfmpo  8045  mpoxeldm  8154  mpocurryd  8212  mpocurryvald  8213  fvmpocurryd  8214  eqerlem  8672  qliftfuns  8744  mptelixpg  8876  boxcutc  8882  xpf1o  9070  iunfi  9246  wdom2d  9488  ixpiunwdom  9498  hsmexlem2  10340  ac6c4  10394  iundom2g  10453  seqof2  14013  rlimcld2  15531  nfsum1  15643  sumeq2ii  15646  summolem3  15667  summolem2a  15668  zsum  15671  fsum  15673  sumss2  15679  fsumcvg2  15680  fsumclf  15691  fsumzcl2  15692  fsumsplitf  15695  sumsnf  15696  sumsns  15703  fsummsnunz  15707  fsumsplitsnun  15708  fsum2dlem  15723  fsumcom2  15727  fsumshftm  15734  fsum0diag2  15736  fsum00  15752  fsumabs  15755  fsumrlim  15765  fsumo1  15766  o1fsum  15767  fsumiun  15775  infcvgaux1i  15813  nfcprod1  15864  prodeq2ii  15867  prodmolem3  15889  prodmolem2a  15890  zprod  15893  fprod  15897  fprodntriv  15898  prodss  15903  fprodser  15905  fprodcllemf  15914  prodsn  15918  prodsnf  15920  fprodm1s  15926  fprodp1s  15927  prodsns  15928  fprodabs  15930  fprodn0  15935  fprod2dlem  15936  fprodcom2  15940  fproddivf  15943  fprodsplitf  15944  fprodsplit1f  15946  fprodle  15952  fprodmodd  15953  fprodefsum  16051  sumeven  16347  sumodd  16348  pcmpt  16854  pcmptdvds  16856  natpropd  17937  fucpropd  17938  gsummpt1n0  19931  gsumcom2  19941  gsummptnn0fz  19952  dprd2d2  20012  psrass1lem  21922  mpfrcl  22073  coe1fzgsumdlem  22278  gsummoncoe1  22283  gsumply1eq  22284  evl1gsumdlem  22331  mdetralt2  22584  mdetunilem2  22588  madugsum  22618  fiuncmp  23379  ptcld  23588  ptcldmpt  23589  ptclsg  23590  elmptrab  23802  prdsdsf  24342  prdsxmet  24344  fsumcn  24847  fsum2cn  24848  ovolfiniun  25478  ovoliunlem3  25481  ovoliun  25482  ovoliun2  25483  ovoliunnul  25484  finiunmbl  25521  volfiniun  25524  iundisj  25525  iundisj2  25526  iunmbl  25530  iunmbl2  25534  itgss3  25792  itgfsum  25804  itgabs  25812  limciun  25871  dvmptfsum  25952  dvfsumle  25998  dvfsumabs  26000  dvfsumlem1  26003  dvfsumlem2  26004  dvfsumlem3  26005  dvfsumlem4  26006  dvfsumrlim  26008  dvfsumrlim2  26009  dvfsum2  26011  itgsubstlem  26025  itgsubst  26026  rlimcnp2  26943  fsumdvdscom  27162  fsumdvdsmul  27172  fsumvma  27190  dchrisumlema  27465  dchrisumlem2  27467  dchrisumlem3  27468  iunxpssiun1  32653  disjorsf  32665  disjabrex  32667  disjabrexf  32668  iundisjf  32674  iundisj2f  32675  disjunsn  32679  suppss2f  32726  2ndresdju  32737  fmptdF  32744  fmptcof2  32745  acunirnmpt2f  32749  aciunf1lem  32750  funcnv4mpt  32756  f1od2  32807  iundisjfi  32884  iundisj2fi  32885  fsumiunle  32917  gsummpt2co  33124  gsummptp1  33133  gsumpart  33139  gsumvsca1  33302  gsumvsca2  33303  rmfsupp2  33314  esumpfinvalf  34236  esum2dlem  34252  esumiun  34254  fiunelros  34334  measiun  34378  voliune  34389  volfiniune  34390  sbcaltop  36179  weiunpo  36663  weiunso  36664  weiunfr  36665  weiunse  36666  csbttc  36707  bj-sbeqALT  37223  phpreu  37939  finixpnum  37940  ptrest  37954  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  mbfposadd  38002  itgabsnc  38024  ftc1cnnclem  38026  ftc2nc  38037  fsumshftd  39412  riotasv2s  39418  cdleme31sn  40840  cdleme31sn1  40841  cdleme31se2  40843  cdleme32fva  40897  cdleme42b  40938  hlhilset  42394  evl1gprodd  42570  idomnnzgmulnz  42586  deg1gprod  42593  fmpocos  42689  mzpsubst  43194  rabdiophlem2  43248  elnn0rabdioph  43249  dvdsrabdioph  43256  fphpd  43262  monotuz  43387  oddcomabszz  43390  wdom2d2  43481  aomclem6  43505  flcidc  43616  fsumcnf  45470  sumsnd  45475  fiiuncl  45514  eliin2f  45552  disjf1  45631  disjrnmpt2  45636  disjinfi  45640  fmptf  45686  fmptff  45716  iuneqfzuzlem  45782  supxrleubrnmptf  45897  fsummulc1f  46019  fsumnncl  46020  fsumf1of  46022  fsumiunss  46023  fsumreclf  46024  fsumlessf  46025  fprodexp  46042  fprodabs2  46043  mccllem  46045  fprodcnlem  46047  fprodcn  46048  climeldmeqmpt  46114  climeldmeqmpt3  46135  climinf2mpt  46160  climinfmpt  46161  limsupequzmptf  46177  fprodcncf  46346  dvmptmulf  46383  dvnmptdivc  46384  dvmptfprod  46391  iblsplitf  46416  fourierdlem86  46638  fourierdlem112  46664  sge0f1o  46828  sge0iunmptlemfi  46859  sge0iunmptlemre  46861  sge0iunmpt  46864  sge0ltfirpmpt2  46872  sge0isummpt2  46878  sge0xaddlem2  46880  sge0xadd  46881  hoimbl2  47111  vonn0ioo2  47136  vonn0icc2  47138  csbafv12g  47597  csbaovg  47640  csbafv212g  47679  fsummsndifre  47840  fsumsplitsndif  47841  fsummmodsndifre  47842  fsummmodsnunz  47843  dmmpossx2  48825