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

Theorem sbcg 3654
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3652. (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 1995 . 2 𝑥𝜑
21sbcgf 3652 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2145  [wsbc 3588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353  df-sbc 3589
This theorem is referenced by:  sbcabel  3667  csbuni  4603  csbxp  5341  sbcfung  6056  fmptsnd  6580  f1od2  29840  bnj89  31128  bnj525  31146  bnj1128  31397  csbwrecsg  33511  csbrdgg  33513  csboprabg  33514  mptsnunlem  33523  topdifinffinlem  33533  relowlpssretop  33550  rdgeqoa  33556  csbfinxpg  33563  sbtru  34241  sbfal  34242  cdlemk40  36727  cdlemkid3N  36743  cdlemkid4  36744  frege70  38754  frege77  38761  frege116  38800  frege118  38802  trsbc  39276  csbxpgOLD  39577  csbxpgVD  39653  csbunigVD  39657
  Copyright terms: Public domain W3C validator