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

Theorem sbcg 3536
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3534. (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 1883 . 2 𝑥𝜑
21sbcgf 3534 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2030  [wsbc 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-sbc 3469
This theorem is referenced by:  sbcabel  3550  csbuni  4498  csbxp  5234  sbcfung  5950  fmptsnd  6476  f1od2  29627  bnj89  30915  bnj525  30933  bnj1128  31184  csbwrecsg  33303  csbrdgg  33305  csboprabg  33306  mptsnunlem  33315  topdifinffinlem  33325  relowlpssretop  33342  rdgeqoa  33348  csbfinxpg  33355  sbtru  34038  sbfal  34039  cdlemk40  36522  cdlemkid3N  36538  cdlemkid4  36539  frege70  38544  frege77  38551  frege116  38590  frege118  38592  trsbc  39067  csbxpgOLD  39368  csbxpgVD  39444  csbunigVD  39448
  Copyright terms: Public domain W3C validator