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

Theorem csbconstg 3447
 Description: Substitution doesn't affect a constant (in which does not occur). csbconstgf 3446 with distinct variable requirement. (Contributed by Alan Sare, 22-Jul-2012.)
Assertion
Ref Expression
csbconstg
Distinct variable group:   ,

Proof of Theorem csbconstg
StepHypRef Expression
1 nfcv 2619 . 2
21csbconstgf 3446 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  [_csb 3434 This theorem is referenced by:  csb0  3822  sbcel1g  3829  sbceq1g  3830  sbcel2  3831  sbcel2gOLD  3832  sbceq2g  3833  csbidm  3846  csbidmgOLD  3847  sbcbr  4505  sbcbr12g  4506  sbcbr1g  4507  sbcbr2g  4508  csbmpt12  4786  csbmpt2  4787  sbcrel  5094  csbcnvgALT  5192  csbres  5281  csbresgOLD  5282  csbrn  5473  sbcfung  5616  csbfv12  5906  csbfv12gOLD  5907  csbfv2g  5908  elfvmptrab  5977  csbov  6331  csbov12g  6333  csbov1g  6334  csbov2g  6335  csbwrdg  12570  gsummptif1n0  16993  coe1fzgsumdlem  18343  evl1gsumdlem  18392  rusgrasn  24945  disjpreima  27445  csbconstgi  30522  onfrALTlem5  33314  onfrALTlem4  33315  csbfv12gALTOLD  33621  onfrALTlem5VD  33685  onfrALTlem4VD  33686  csbsngVD  33693  csbxpgVD  33694  csbresgVD  33695  csbrngVD  33696  csbfv12gALTVD  33699  cdlemkid3N  36659  cdlemkid4  36660  cdlemk42  36667 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sbc 3328  df-csb 3435
 Copyright terms: Public domain W3C validator