Theorem nfcsb1v 3861

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

Syntax hints:  Ⅎwnfc 2888  ⦋csb 3836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-sbc 3720  df-csb 3837

This theorem is referenced by:  csbhypf  3865  csbiebt  3866  cbvrabcsfw  3880  cbvralcsf  3881  cbvreucsf  3883  cbvrabcsf  3884  rspc2vd  3887  sbcnestgfw  4357  sbcnestgf  4362  csbnest1g  4368  csbun  4377  csbin  4378  csbdif  4463  csbif  4521  disjors  5059  invdisjrabw  5063  invdisjrab  5064  disjxiun  5075  disjxun  5076  sbcbr123  5132  eusvnf  5318  reusv2lem4  5327  reusv2  5329  moop2  5418  iunopeqop  5437  pofun  5520  opeliunxp  5653  elrnmpt1  5864  resmptf  5944  csbima12  5984  csbcog  6197  fvmpt2f  6870  fvmpts  6872  fvmptdf  6875  fvmpt2i  6879  fvmptex  6883  fmptco  6995  fmptcof  6996  fmptcos  6997  elabrex  7110  fliftfuns  7178  csbov123  7310  ovmpos  7412  fvmpopr2d  7425  ofmpteq  7546  mpomptsx  7890  dmmpossx  7892  fmpox  7893  el2mpocsbcl  7909  offval22  7912  ovmptss  7917  fmpoco  7919  dfmpo  7926  mpoxeldm  8011  mpocurryd  8069  mpocurryvald  8070  fvmpocurryd  8071  eqerlem  8506  qliftfuns  8567  mptelixpg  8697  boxcutc  8703  xpf1o  8891  iunfi  9068  wdom2d  9300  ixpiunwdom  9310  hsmexlem2  10167  ac6c4  10221  iundom2g  10280  seqof2  13762  rlimcld2  15268  nfsum1  15382  sumeq2ii  15386  summolem3  15407  summolem2a  15408  zsum  15411  fsum  15413  sumss2  15419  fsumcvg2  15420  fsumclf  15431  fsumzcl2  15432  fsumsplitf  15435  sumsnf  15436  sumsns  15443  fsummsnunz  15447  fsumsplitsnun  15448  fsum2dlem  15463  fsumcom2  15467  fsumshftm  15474  fsum0diag2  15476  fsum00  15491  fsumabs  15494  fsumrlim  15504  fsumo1  15505  o1fsum  15506  fsumiun  15514  infcvgaux1i  15550  nfcprod1  15601  prodeq2ii  15604  prodmolem3  15624  prodmolem2a  15625  zprod  15628  fprod  15632  fprodntriv  15633  prodss  15638  fprodser  15640  fprodcllemf  15649  prodsn  15653  prodsnf  15655  fprodm1s  15661  fprodp1s  15662  prodsns  15663  fprodabs  15665  fprodn0  15670  fprod2dlem  15671  fprodcom2  15675  fproddivf  15678  fprodsplitf  15679  fprodsplit1f  15681  fprodle  15687  fprodmodd  15688  fprodefsum  15785  sumeven  16077  sumodd  16078  pcmpt  16574  pcmptdvds  16576  natpropd  17675  fucpropd  17676  gsummpt1n0  19547  gsumcom2  19557  gsummptnn0fz  19568  dprd2d2  19628  psrass1lemOLD  21124  psrass1lem  21127  mpfrcl  21276  coe1fzgsumdlem  21453  gsummoncoe1  21456  gsumply1eq  21457  evl1gsumdlem  21503  mdetralt2  21739  mdetunilem2  21743  madugsum  21773  fiuncmp  22536  ptcld  22745  ptcldmpt  22746  ptclsg  22747  elmptrab  22959  prdsdsf  23501  prdsxmet  23503  fsumcn  24014  fsum2cn  24015  ovolfiniun  24646  ovoliunlem3  24649  ovoliun  24650  ovoliun2  24651  ovoliunnul  24652  finiunmbl  24689  volfiniun  24692  iundisj  24693  iundisj2  24694  iunmbl  24698  iunmbl2  24702  itgss3  24960  itgfsum  24972  itgabs  24980  limciun  25039  dvmptfsum  25120  dvfsumle  25166  dvfsumabs  25168  dvfsumlem1  25171  dvfsumlem2  25172  dvfsumlem3  25173  dvfsumlem4  25174  dvfsumrlim  25176  dvfsumrlim2  25177  dvfsum2  25179  itgsubstlem  25193  itgsubst  25194  rlimcnp2  26097  fsumdvdscom  26315  fsumdvdsmul  26325  fsumvma  26342  dchrisumlema  26617  dchrisumlem2  26619  dchrisumlem3  26620  disjorsf  30898  disjabrex  30900  disjabrexf  30901  iundisjf  30907  iundisj2f  30908  disjunsn  30912  suppss2f  30953  2ndresdju  30965  fmptdF  30972  fmptcof2  30973  acunirnmpt2f  30977  aciunf1lem  30978  funcnv4mpt  30985  f1od2  31035  iundisjfi  31096  iundisj2fi  31097  fsumiunle  31122  gsummpt2co  31287  gsumpart  31294  gsumvsca1  31458  gsumvsca2  31459  rmfsupp2  31471  esumpfinvalf  32023  esum2dlem  32039  esumiun  32041  fiunelros  32121  measiun  32165  voliune  32176  volfiniune  32177  sbcaltop  34262  bj-sbeqALT  35064  phpreu  35740  finixpnum  35741  ptrest  35755  poimirlem23  35779  poimirlem24  35780  poimirlem25  35781  poimirlem26  35782  poimirlem27  35783  poimirlem28  35784  mbfposadd  35803  itgabsnc  35825  ftc1cnnclem  35827  ftc2nc  35838  fsumshftd  36945  riotasv2s  36951  cdleme31sn  38373  cdleme31sn1  38374  cdleme31se2  38376  cdleme32fva  38430  cdleme42b  38471  hlhilset  39927  mzpsubst  40550  rabdiophlem2  40604  elnn0rabdioph  40605  dvdsrabdioph  40612  fphpd  40618  monotuz  40743  oddcomabszz  40746  wdom2d2  40837  aomclem6  40864  flcidc  40979  fsumcnf  42517  sumsnd  42522  elabrexg  42542  fiiuncl  42566  eliin2f  42607  disjf1  42673  disjrnmpt2  42679  disjinfi  42684  fmptf  42736  iuneqfzuzlem  42827  supxrleubrnmptf  42945  fsummulc1f  43066  fsumnncl  43067  fsumf1of  43069  fsumiunss  43070  fsumreclf  43071  fsumlessf  43072  fprodexp  43089  fprodabs2  43090  mccllem  43092  fprodcnlem  43094  fprodcn  43095  climeldmeqmpt  43163  climeldmeqmpt3  43184  climinf2mpt  43209  climinfmpt  43210  limsupequzmptf  43226  fprodcncf  43395  dvmptmulf  43432  dvnmptdivc  43433  dvmptfprod  43440  iblsplitf  43465  fourierdlem86  43687  fourierdlem112  43713  sge0iunmptlemfi  43905  sge0iunmptlemre  43907  sge0iunmpt  43910  sge0ltfirpmpt2  43918  sge0isummpt2  43924  sge0xaddlem2  43926  sge0xadd  43927  hoimbl2  44157  vonn0ioo2  44182  vonn0icc2  44184  csbafv12g  44580  csbaovg  44623  csbafv212g  44662  fsummsndifre  44776  fsumsplitsndif  44777  fsummmodsndifre  44778  fsummmodsnunz  44779  opeliun2xp  45620  dmmpossx2  45624