MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbconstg Structured version   Visualization version   GIF version

Theorem csbconstg 3683
Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3682 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
Assertion
Ref Expression
csbconstg (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐵)
Distinct variable group:   𝑥,𝐵
Allowed substitution hints:   𝐴(𝑥)   𝑉(𝑥)

Proof of Theorem csbconstg
StepHypRef Expression
1 nfcv 2898 . 2 𝑥𝐵
21csbconstgf 3682 1 (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1628  wcel 2135  csb 3670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-v 3338  df-sbc 3573  df-csb 3671
This theorem is referenced by:  csb0  4121  sbcel1g  4126  sbceq1g  4127  sbcel2  4128  sbceq2g  4129  csbidm  4141  csbopg  4567  sbcbr  4855  sbcbr12g  4856  sbcbr1g  4857  sbcbr2g  4858  csbmpt12  5156  csbmpt2  5157  sbcrel  5358  csbcnvgALT  5458  csbres  5550  csbrn  5750  sbcfung  6069  csbfv12  6388  csbfv2g  6389  elfvmptrab  6464  csbov  6847  csbov12g  6848  csbov1g  6849  csbov2g  6850  csbwrdg  13516  gsummptif1n0  18561  coe1fzgsumdlem  19869  evl1gsumdlem  19918  disjpreima  29700  esum2dlem  30459  csbwrecsg  33480  csbrecsg  33481  csbrdgg  33482  csbmpt22g  33484  f1omptsnlem  33490  relowlpssretop  33519  rdgeqoa  33525  csbfinxpg  33532  csbconstgi  34231  cdlemkid3N  36719  cdlemkid4  36720  cdlemk42  36727  brtrclfv2  38517  cotrclrcl  38532  frege77  38732  sbcel2gOLD  39253  onfrALTlem5  39255  onfrALTlem4  39256  csbresgOLD  39551  onfrALTlem5VD  39616  onfrALTlem4VD  39617  csbsngVD  39624  csbxpgVD  39625  csbresgVD  39626  csbrngVD  39627  csbfv12gALTVD  39630  disjinfi  39875  iccelpart  41875
  Copyright terms: Public domain W3C validator