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

Theorem csbconstg 3741
Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3740 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 2948 . 2 𝑥𝐵
21csbconstgf 3740 1 (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2156  csb 3728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-sbc 3634  df-csb 3729
This theorem is referenced by:  csb0  4179  sbcel1g  4184  sbceq1g  4185  sbcel2  4186  sbceq2g  4187  csbidm  4199  csbopg  4613  sbcbr  4899  sbcbr12g  4900  sbcbr1g  4901  sbcbr2g  4902  csbmpt12  5205  csbmpt2  5206  sbcrel  5407  csbcnvgALT  5508  csbres  5600  csbrn  5807  sbcfung  6125  csbfv12  6451  csbfv2g  6452  elfvmptrab  6527  csbov  6916  csbov12g  6917  csbov1g  6918  csbov2g  6919  csbwrdg  13545  gsummptif1n0  18566  coe1fzgsumdlem  19879  evl1gsumdlem  19928  disjpreima  29722  esum2dlem  30479  csbwrecsg  33490  csbrecsg  33491  csbrdgg  33492  csbmpt22g  33494  f1omptsnlem  33500  relowlpssretop  33528  rdgeqoa  33534  csbfinxpg  33541  csbconstgi  34232  cdlemkid3N  36714  cdlemkid4  36715  cdlemk42  36722  brtrclfv2  38519  cotrclrcl  38534  frege77  38734  sbcel2gOLD  39253  onfrALTlem5  39255  onfrALTlem4  39256  csbresgOLD  39550  onfrALTlem5VD  39615  onfrALTlem4VD  39616  csbsngVD  39623  csbxpgVD  39624  csbresgVD  39625  csbrngVD  39626  csbfv12gALTVD  39629  disjinfi  39869  eubrdm  41655  iccelpart  41944
  Copyright terms: Public domain W3C validator