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

Theorem csbconstg 3850
Description: Substitution doesn't affect a constant 𝐵 (in which 𝑥 does not occur). csbconstgf 3849 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 2958 . 2 𝑥𝐵
21csbconstgf 3849 1 (𝐴𝑉𝐴 / 𝑥𝐵 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112  csb 3831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-sbc 3724  df-csb 3832
This theorem is referenced by:  csbconstgi  3852  csb0OLD  4318  sbcel1g  4324  sbceq1g  4325  sbcel2  4326  sbceq2g  4327  csbidm  4341  2nreu  4352  csbopg  4786  sbcbr  5088  sbcbr12g  5089  sbcbr1g  5090  sbcbr2g  5091  csbmpt12  5412  csbmpt2  5413  sbcrel  5623  csbcnvgALT  5723  csbres  5825  csbrn  6031  sbcfung  6352  csbfv12  6692  csbfv2g  6693  elfvmptrab  6777  csbov  7182  csbov12g  7183  csbov1g  7184  csbov2g  7185  csbwrdg  13891  gsummptif1n0  19082  coe1fzgsumdlem  20933  evl1gsumdlem  20983  opsbc2ie  30249  disjpreima  30350  esum2dlem  31459  csbwrecsg  34739  csbrecsg  34740  csbrdgg  34741  csbmpo123  34743  f1omptsnlem  34748  relowlpssretop  34776  rdgeqoa  34782  csbfinxpg  34800  cdlemkid3N  38222  cdlemkid4  38223  cdlemk42  38230  brtrclfv2  40415  cotrclrcl  40430  frege77  40628  onfrALTlem5  41235  onfrALTlem4  41236  onfrALTlem5VD  41578  onfrALTlem4VD  41579  csbsngVD  41586  csbxpgVD  41587  csbresgVD  41588  csbrngVD  41589  csbfv12gALTVD  41592  disjinfi  41807  eubrdm  43615  iccelpart  43937
  Copyright terms: Public domain W3C validator