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

Theorem sbcg 3401
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3399. (Contributed by Alan Sare, 10-Nov-2012.)
Assertion
Ref Expression
sbcg
Distinct variable group:   ,

Proof of Theorem sbcg
StepHypRef Expression
1 nfv 1707 . 2
21sbcgf 3399 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  [.wsbc 3327
This theorem is referenced by:  sbcabel  3416  csbuni  4277  csbunigOLD  4278  csbxp  5086  csbxpgOLD  5087  sbcfung  5616  fmptsnd  6093  f1od2  27547  sbtru  30508  sbfal  30509  trsbc  33311  csbxpgVD  33694  csbunigVD  33698  bnj89  33774  bnj525  33794  bnj1128  34046  cdlemk40  36643  cdlemkid3N  36659  cdlemkid4  36660
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-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-v 3111  df-sbc 3328
  Copyright terms: Public domain W3C validator