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

Theorem sbcg 3795
 Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3793. (Contributed by Alan Sare, 10-Nov-2012.)
Assertion
Ref Expression
sbcg (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜑))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝑉(𝑥)

Proof of Theorem sbcg
StepHypRef Expression
1 nfv 1915 . 2 𝑥𝜑
21sbcgf 3793 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2111  [wsbc 3722 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 2113  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3723 This theorem is referenced by:  sbcabel  3809  2nreu  4352  csbuni  4833  csbxp  5618  sbcfung  6356  fmptsnd  6918  opsbc2ie  30290  f1od2  30527  bnj89  32167  bnj525  32185  bnj1128  32438  csbwrecsg  34895  csbrdgg  34897  csboprabg  34898  mptsnunlem  34906  topdifinffinlem  34915  relowlpssretop  34932  rdgeqoa  34938  csbfinxpg  34956  gm-sbtru  35695  sbfal  35696  cdlemk40  38364  cdlemkid3N  38380  cdlemkid4  38381  frege70  40805  frege77  40812  frege116  40851  frege118  40853  trsbc  41417  trsbcVD  41754  csbxpgVD  41771  csbunigVD  41775
 Copyright terms: Public domain W3C validator