Theorem nfcsb1v 3870

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

Syntax hints:  Ⅎwnfc 2880  ⦋csb 3846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-sbc 3738  df-csb 3847

This theorem is referenced by:  csbhypf  3874  csbiebt  3875  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  rspc2vd  3894  sbcnestgfw  4370  sbcnestgf  4375  csbnest1g  4381  csbun  4390  csbin  4391  csbdif  4475  csbif  4534  disjors  5078  invdisjrab  5082  disjxiun  5092  disjxun  5093  sbcbr123  5149  eusvnf  5334  reusv2lem4  5343  reusv2  5345  moop2  5447  iunopeqop  5466  pofun  5547  opeliunxp  5688  opeliun2xp  5689  elrnmpt1  5906  resmptf  5994  csbima12  6034  csbcog  6251  fvmpt2f  6938  fvmpts  6940  fvmptdf  6943  fvmpt2i  6947  fvmptex  6951  fmptco  7070  fmptcof  7071  fmptcos  7072  elabrex  7184  elabrexg  7185  fliftfuns  7256  csbov123  7398  ovmpos  7502  fvmpopr2d  7516  ofmpteq  7641  mpomptsx  8004  dmmpossx  8006  fmpox  8007  el2mpocsbcl  8023  offval22  8026  ovmptss  8031  fmpoco  8033  dfmpo  8040  mpoxeldm  8149  mpocurryd  8207  mpocurryvald  8208  fvmpocurryd  8209  eqerlem  8665  qliftfuns  8736  mptelixpg  8867  boxcutc  8873  xpf1o  9061  iunfi  9236  wdom2d  9475  ixpiunwdom  9485  hsmexlem2  10327  ac6c4  10381  iundom2g  10440  seqof2  13971  rlimcld2  15489  nfsum1  15601  sumeq2ii  15604  summolem3  15625  summolem2a  15626  zsum  15629  fsum  15631  sumss2  15637  fsumcvg2  15638  fsumclf  15649  fsumzcl2  15650  fsumsplitf  15653  sumsnf  15654  sumsns  15661  fsummsnunz  15665  fsumsplitsnun  15666  fsum2dlem  15681  fsumcom2  15685  fsumshftm  15692  fsum0diag2  15694  fsum00  15709  fsumabs  15712  fsumrlim  15722  fsumo1  15723  o1fsum  15724  fsumiun  15732  infcvgaux1i  15768  nfcprod1  15819  prodeq2ii  15822  prodmolem3  15844  prodmolem2a  15845  zprod  15848  fprod  15852  fprodntriv  15853  prodss  15858  fprodser  15860  fprodcllemf  15869  prodsn  15873  prodsnf  15875  fprodm1s  15881  fprodp1s  15882  prodsns  15883  fprodabs  15885  fprodn0  15890  fprod2dlem  15891  fprodcom2  15895  fproddivf  15898  fprodsplitf  15899  fprodsplit1f  15901  fprodle  15907  fprodmodd  15908  fprodefsum  16006  sumeven  16302  sumodd  16303  pcmpt  16808  pcmptdvds  16810  natpropd  17890  fucpropd  17891  gsummpt1n0  19881  gsumcom2  19891  gsummptnn0fz  19902  dprd2d2  19962  psrass1lem  21873  mpfrcl  22023  coe1fzgsumdlem  22221  gsummoncoe1  22226  gsumply1eq  22227  evl1gsumdlem  22274  mdetralt2  22527  mdetunilem2  22531  madugsum  22561  fiuncmp  23322  ptcld  23531  ptcldmpt  23532  ptclsg  23533  elmptrab  23745  prdsdsf  24285  prdsxmet  24287  fsumcn  24791  fsum2cn  24792  ovolfiniun  25432  ovoliunlem3  25435  ovoliun  25436  ovoliun2  25437  ovoliunnul  25438  finiunmbl  25475  volfiniun  25478  iundisj  25479  iundisj2  25480  iunmbl  25484  iunmbl2  25488  itgss3  25746  itgfsum  25758  itgabs  25766  limciun  25825  dvmptfsum  25909  dvfsumle  25956  dvfsumleOLD  25957  dvfsumabs  25959  dvfsumlem1  25962  dvfsumlem2  25963  dvfsumlem2OLD  25964  dvfsumlem3  25965  dvfsumlem4  25966  dvfsumrlim  25968  dvfsumrlim2  25969  dvfsum2  25971  itgsubstlem  25985  itgsubst  25986  rlimcnp2  26906  fsumdvdscom  27125  fsumdvdsmul  27135  fsumdvdsmulOLD  27137  fsumvma  27154  dchrisumlema  27429  dchrisumlem2  27431  dchrisumlem3  27432  iunxpssiun1  32552  disjorsf  32564  disjabrex  32566  disjabrexf  32567  iundisjf  32573  iundisj2f  32574  disjunsn  32578  suppss2f  32624  2ndresdju  32635  fmptdF  32642  fmptcof2  32643  acunirnmpt2f  32647  aciunf1lem  32648  funcnv4mpt  32655  f1od2  32708  iundisjfi  32785  iundisj2fi  32786  fsumiunle  32819  gsummpt2co  33037  gsumpart  33046  gsumvsca1  33204  gsumvsca2  33205  rmfsupp2  33214  esumpfinvalf  34112  esum2dlem  34128  esumiun  34130  fiunelros  34210  measiun  34254  voliune  34265  volfiniune  34266  sbcaltop  36048  weiunpo  36532  weiunso  36533  weiunfr  36534  weiunse  36535  bj-sbeqALT  36967  phpreu  37667  finixpnum  37668  ptrest  37682  poimirlem23  37706  poimirlem24  37707  poimirlem25  37708  poimirlem26  37709  poimirlem27  37710  poimirlem28  37711  mbfposadd  37730  itgabsnc  37752  ftc1cnnclem  37754  ftc2nc  37765  fsumshftd  39074  riotasv2s  39080  cdleme31sn  40502  cdleme31sn1  40503  cdleme31se2  40505  cdleme32fva  40559  cdleme42b  40600  hlhilset  42056  evl1gprodd  42233  idomnnzgmulnz  42249  deg1gprod  42256  fmpocos  42355  mzpsubst  42868  rabdiophlem2  42922  elnn0rabdioph  42923  dvdsrabdioph  42930  fphpd  42936  monotuz  43061  oddcomabszz  43064  wdom2d2  43155  aomclem6  43179  flcidc  43290  fsumcnf  45145  sumsnd  45150  fiiuncl  45189  eliin2f  45228  disjf1  45307  disjrnmpt2  45312  disjinfi  45316  fmptf  45363  fmptff  45393  iuneqfzuzlem  45460  supxrleubrnmptf  45576  fsummulc1f  45698  fsumnncl  45699  fsumf1of  45701  fsumiunss  45702  fsumreclf  45703  fsumlessf  45704  fprodexp  45721  fprodabs2  45722  mccllem  45724  fprodcnlem  45726  fprodcn  45727  climeldmeqmpt  45793  climeldmeqmpt3  45814  climinf2mpt  45839  climinfmpt  45840  limsupequzmptf  45856  fprodcncf  46025  dvmptmulf  46062  dvnmptdivc  46063  dvmptfprod  46070  iblsplitf  46095  fourierdlem86  46317  fourierdlem112  46343  sge0f1o  46507  sge0iunmptlemfi  46538  sge0iunmptlemre  46540  sge0iunmpt  46543  sge0ltfirpmpt2  46551  sge0isummpt2  46557  sge0xaddlem2  46559  sge0xadd  46560  hoimbl2  46790  vonn0ioo2  46815  vonn0icc2  46817  csbafv12g  47264  csbaovg  47307  csbafv212g  47346  fsummsndifre  47499  fsumsplitsndif  47500  fsummmodsndifre  47501  fsummmodsnunz  47502  dmmpossx2  48464