Theorem nfcsb1v 3824

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

Syntax hints:  Ⅎwnfc 2880  ⦋csb 3800

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-sbc 3686  df-csb 3801

This theorem is referenced by:  csbhypf  3828  csbiebt  3829  cbvrabcsfw  3841  cbvralcsf  3842  cbvreucsf  3844  cbvrabcsf  3845  rspc2vd  3849  sbcnestgfw  4318  sbcnestgf  4323  csbnest1g  4329  csbun  4338  csbin  4339  csbif  4481  disjors  5021  invdisjrabw  5025  invdisjrab  5026  disjxiun  5037  disjxun  5038  sbcbr123  5094  eusvnf  5269  reusv2lem4  5278  reusv2  5280  moop2  5369  iunopeqop  5388  pofun  5470  opeliunxp  5600  elrnmpt1  5811  resmptf  5891  csbima12  5931  fvmpt2f  6789  fvmpts  6791  fvmptdf  6794  fvmpt2i  6798  fvmptex  6802  fmptco  6914  fmptcof  6915  fmptcos  6916  elabrex  7026  fliftfuns  7093  csbov123  7225  ovmpos  7326  fvmpopr2d  7339  ofmpteq  7459  mpomptsx  7800  dmmpossx  7802  fmpox  7803  el2mpocsbcl  7819  offval22  7822  ovmptss  7827  fmpoco  7829  dfmpo  7836  mpoxeldm  7919  mpocurryd  7977  mpocurryvald  7978  fvmpocurryd  7979  eqerlem  8367  qliftfuns  8428  mptelixpg  8558  boxcutc  8564  xpf1o  8742  iunfi  8898  wdom2d  9130  ixpiunwdom  9140  hsmexlem2  9940  ac6c4  9994  iundom2g  10053  seqof2  13533  rlimcld2  15038  nfsum1  15152  sumeq2ii  15156  summolem3  15177  summolem2a  15178  zsum  15181  fsum  15183  sumss2  15189  fsumcvg2  15190  fsumzcl2  15201  fsumsplitf  15204  sumsnf  15205  sumsns  15211  fsummsnunz  15215  fsumsplitsnun  15216  fsum2dlem  15231  fsumcom2  15235  fsumshftm  15242  fsum0diag2  15244  fsum00  15259  fsumabs  15262  fsumrlim  15272  fsumo1  15273  o1fsum  15274  fsumiun  15282  infcvgaux1i  15318  nfcprod1  15369  prodeq2ii  15372  prodmolem3  15392  prodmolem2a  15393  zprod  15396  fprod  15400  fprodntriv  15401  prodss  15406  fprodser  15408  fprodcllemf  15417  prodsn  15421  prodsnf  15423  fprodm1s  15429  fprodp1s  15430  prodsns  15431  fprodabs  15433  fprodn0  15438  fprod2dlem  15439  fprodcom2  15443  fproddivf  15446  fprodsplitf  15447  fprodsplit1f  15449  fprodle  15455  fprodmodd  15456  fprodefsum  15553  sumeven  15845  sumodd  15846  pcmpt  16341  pcmptdvds  16343  natpropd  17364  fucpropd  17365  gsummpt1n0  19217  gsumcom2  19227  gsummptnn0fz  19238  dprd2d2  19298  psrass1lemOLD  20766  psrass1lem  20769  mpfrcl  20912  coe1fzgsumdlem  21089  gsummoncoe1  21092  gsumply1eq  21093  evl1gsumdlem  21139  mdetralt2  21373  mdetunilem2  21377  madugsum  21407  fiuncmp  22168  ptcld  22377  ptcldmpt  22378  ptclsg  22379  elmptrab  22591  prdsdsf  23133  prdsxmet  23135  fsumcn  23635  fsum2cn  23636  ovolfiniun  24266  ovoliunlem3  24269  ovoliun  24270  ovoliun2  24271  ovoliunnul  24272  finiunmbl  24309  volfiniun  24312  iundisj  24313  iundisj2  24314  iunmbl  24318  iunmbl2  24322  itgss3  24580  itgfsum  24592  itgabs  24600  limciun  24659  dvmptfsum  24740  dvfsumle  24786  dvfsumabs  24788  dvfsumlem1  24791  dvfsumlem2  24792  dvfsumlem3  24793  dvfsumlem4  24794  dvfsumrlim  24796  dvfsumrlim2  24797  dvfsum2  24799  itgsubstlem  24813  itgsubst  24814  rlimcnp2  25717  fsumdvdscom  25935  fsumdvdsmul  25945  fsumvma  25962  dchrisumlema  26237  dchrisumlem2  26239  dchrisumlem3  26240  disjorsf  30506  disjabrex  30508  disjabrexf  30509  iundisjf  30515  iundisj2f  30516  disjunsn  30520  suppss2f  30561  2ndresdju  30573  fmptdF  30581  fmptcof2  30582  acunirnmpt2f  30586  aciunf1lem  30587  funcnv4mpt  30594  f1od2  30644  iundisjfi  30705  iundisj2fi  30706  fsumiunle  30731  gsummpt2co  30898  gsumpart  30905  gsumvsca1  31069  gsumvsca2  31070  rmfsupp2  31082  esumpfinvalf  31627  esum2dlem  31643  esumiun  31645  fiunelros  31725  measiun  31769  voliune  31780  volfiniune  31781  sbcaltop  33939  bj-sbeqALT  34742  csbdif  35152  phpreu  35417  finixpnum  35418  ptrest  35432  poimirlem23  35456  poimirlem24  35457  poimirlem25  35458  poimirlem26  35459  poimirlem27  35460  poimirlem28  35461  mbfposadd  35480  itgabsnc  35502  ftc1cnnclem  35504  ftc2nc  35515  fsumshftd  36622  riotasv2s  36628  cdleme31sn  38050  cdleme31sn1  38051  cdleme31se2  38053  cdleme32fva  38107  cdleme42b  38148  hlhilset  39604  mzpsubst  40183  rabdiophlem2  40237  elnn0rabdioph  40238  dvdsrabdioph  40245  fphpd  40251  monotuz  40376  oddcomabszz  40379  wdom2d2  40470  aomclem6  40497  flcidc  40612  csbcog  40844  fsumcnf  42143  sumsnd  42148  elabrexg  42168  fiiuncl  42192  eliin2f  42233  disjf1  42299  disjrnmpt2  42305  disjinfi  42310  fmptf  42361  iuneqfzuzlem  42452  supxrleubrnmptf  42572  fsumclf  42693  fsummulc1f  42694  fsumnncl  42695  fsumf1of  42698  fsumiunss  42699  fsumreclf  42700  fsumlessf  42701  fprodexp  42718  fprodabs2  42719  mccllem  42721  fprodcnlem  42723  fprodcn  42724  climeldmeqmpt  42792  climeldmeqmpt3  42813  climinf2mpt  42838  climinfmpt  42839  limsupequzmptf  42855  fprodcncf  43024  dvmptmulf  43061  dvnmptdivc  43062  dvmptfprod  43069  iblsplitf  43094  fourierdlem86  43316  fourierdlem112  43342  sge0iunmptlemfi  43534  sge0iunmptlemre  43536  sge0iunmpt  43539  sge0ltfirpmpt2  43547  sge0isummpt2  43553  sge0xaddlem2  43555  sge0xadd  43556  hoimbl2  43786  vonn0ioo2  43811  vonn0icc2  43813  csbafv12g  44210  csbaovg  44253  csbafv212g  44292  fsummsndifre  44406  fsumsplitsndif  44407  fsummmodsndifre  44408  fsummmodsnunz  44409  opeliun2xp  45250  dmmpossx2  45254