Theorem nfcsb1v 3923

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

Syntax hints:  Ⅎwnfc 2890  ⦋csb 3899

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-sbc 3789  df-csb 3900

This theorem is referenced by:  csbhypf  3927  csbiebt  3928  cbvrabcsfw  3940  cbvralcsf  3941  cbvreucsf  3943  cbvrabcsf  3944  rspc2vd  3947  sbcnestgfw  4421  sbcnestgf  4426  csbnest1g  4432  csbun  4441  csbin  4442  csbdif  4524  csbif  4583  disjors  5126  invdisjrab  5130  disjxiun  5140  disjxun  5141  sbcbr123  5197  eusvnf  5392  reusv2lem4  5401  reusv2  5403  moop2  5507  iunopeqop  5526  pofun  5610  opeliunxp  5752  opeliun2xp  5753  elrnmpt1  5971  resmptf  6057  csbima12  6097  csbcog  6317  fvmpt2f  7017  fvmpts  7019  fvmptdf  7022  fvmpt2i  7026  fvmptex  7030  fmptco  7149  fmptcof  7150  fmptcos  7151  elabrex  7262  elabrexg  7263  fliftfuns  7334  csbov123  7475  ovmpos  7581  fvmpopr2d  7595  ofmpteq  7720  mpomptsx  8089  dmmpossx  8091  fmpox  8092  el2mpocsbcl  8110  offval22  8113  ovmptss  8118  fmpoco  8120  dfmpo  8127  mpoxeldm  8236  mpocurryd  8294  mpocurryvald  8295  fvmpocurryd  8296  eqerlem  8780  qliftfuns  8844  mptelixpg  8975  boxcutc  8981  xpf1o  9179  iunfi  9383  wdom2d  9620  ixpiunwdom  9630  hsmexlem2  10467  ac6c4  10521  iundom2g  10580  seqof2  14101  rlimcld2  15614  nfsum1  15726  sumeq2ii  15729  summolem3  15750  summolem2a  15751  zsum  15754  fsum  15756  sumss2  15762  fsumcvg2  15763  fsumclf  15774  fsumzcl2  15775  fsumsplitf  15778  sumsnf  15779  sumsns  15786  fsummsnunz  15790  fsumsplitsnun  15791  fsum2dlem  15806  fsumcom2  15810  fsumshftm  15817  fsum0diag2  15819  fsum00  15834  fsumabs  15837  fsumrlim  15847  fsumo1  15848  o1fsum  15849  fsumiun  15857  infcvgaux1i  15893  nfcprod1  15944  prodeq2ii  15947  prodmolem3  15969  prodmolem2a  15970  zprod  15973  fprod  15977  fprodntriv  15978  prodss  15983  fprodser  15985  fprodcllemf  15994  prodsn  15998  prodsnf  16000  fprodm1s  16006  fprodp1s  16007  prodsns  16008  fprodabs  16010  fprodn0  16015  fprod2dlem  16016  fprodcom2  16020  fproddivf  16023  fprodsplitf  16024  fprodsplit1f  16026  fprodle  16032  fprodmodd  16033  fprodefsum  16131  sumeven  16424  sumodd  16425  pcmpt  16930  pcmptdvds  16932  natpropd  18024  fucpropd  18025  gsummpt1n0  19983  gsumcom2  19993  gsummptnn0fz  20004  dprd2d2  20064  psrass1lem  21952  mpfrcl  22109  coe1fzgsumdlem  22307  gsummoncoe1  22312  gsumply1eq  22313  evl1gsumdlem  22360  mdetralt2  22615  mdetunilem2  22619  madugsum  22649  fiuncmp  23412  ptcld  23621  ptcldmpt  23622  ptclsg  23623  elmptrab  23835  prdsdsf  24377  prdsxmet  24379  fsumcn  24894  fsum2cn  24895  ovolfiniun  25536  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  ovoliunnul  25542  finiunmbl  25579  volfiniun  25582  iundisj  25583  iundisj2  25584  iunmbl  25588  iunmbl2  25592  itgss3  25850  itgfsum  25862  itgabs  25870  limciun  25929  dvmptfsum  26013  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsumrlim  26072  dvfsumrlim2  26073  dvfsum2  26075  itgsubstlem  26089  itgsubst  26090  rlimcnp2  27009  fsumdvdscom  27228  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  fsumvma  27257  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  iunxpssiun1  32581  disjorsf  32593  disjabrex  32595  disjabrexf  32596  iundisjf  32602  iundisj2f  32603  disjunsn  32607  suppss2f  32648  2ndresdju  32659  fmptdF  32666  fmptcof2  32667  acunirnmpt2f  32671  aciunf1lem  32672  funcnv4mpt  32679  f1od2  32732  iundisjfi  32798  iundisj2fi  32799  fsumiunle  32831  gsummpt2co  33051  gsumpart  33060  gsumvsca1  33232  gsumvsca2  33233  rmfsupp2  33242  esumpfinvalf  34077  esum2dlem  34093  esumiun  34095  fiunelros  34175  measiun  34219  voliune  34230  volfiniune  34231  sbcaltop  35982  weiunpo  36466  weiunso  36467  weiunfr  36468  weiunse  36469  bj-sbeqALT  36901  phpreu  37611  finixpnum  37612  ptrest  37626  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  mbfposadd  37674  itgabsnc  37696  ftc1cnnclem  37698  ftc2nc  37709  fsumshftd  38953  riotasv2s  38959  cdleme31sn  40382  cdleme31sn1  40383  cdleme31se2  40385  cdleme32fva  40439  cdleme42b  40480  hlhilset  41936  evl1gprodd  42118  idomnnzgmulnz  42134  deg1gprod  42141  fmpocos  42275  mzpsubst  42759  rabdiophlem2  42813  elnn0rabdioph  42814  dvdsrabdioph  42821  fphpd  42827  monotuz  42953  oddcomabszz  42956  wdom2d2  43047  aomclem6  43071  flcidc  43182  fsumcnf  45026  sumsnd  45031  fiiuncl  45070  eliin2f  45109  disjf1  45188  disjrnmpt2  45193  disjinfi  45197  fmptf  45245  fmptff  45276  iuneqfzuzlem  45345  supxrleubrnmptf  45462  fsummulc1f  45586  fsumnncl  45587  fsumf1of  45589  fsumiunss  45590  fsumreclf  45591  fsumlessf  45592  fprodexp  45609  fprodabs2  45610  mccllem  45612  fprodcnlem  45614  fprodcn  45615  climeldmeqmpt  45683  climeldmeqmpt3  45704  climinf2mpt  45729  climinfmpt  45730  limsupequzmptf  45746  fprodcncf  45915  dvmptmulf  45952  dvnmptdivc  45953  dvmptfprod  45960  iblsplitf  45985  fourierdlem86  46207  fourierdlem112  46233  sge0f1o  46397  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0ltfirpmpt2  46441  sge0isummpt2  46447  sge0xaddlem2  46449  sge0xadd  46450  hoimbl2  46680  vonn0ioo2  46705  vonn0icc2  46707  csbafv12g  47149  csbaovg  47192  csbafv212g  47231  fsummsndifre  47359  fsumsplitsndif  47360  fsummmodsndifre  47361  fsummmodsnunz  47362  dmmpossx2  48253