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

Theorem sbcg 3355
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3353. (Contributed by Alan Sare, 10-Nov-2012.)
Assertion
Ref Expression
sbcg  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ph ) )
Distinct variable group:    ph, x
Allowed substitution hints:    A( x)    V( x)

Proof of Theorem sbcg
StepHypRef Expression
1 nfv 1674 . 2  |-  F/ x ph
21sbcgf 3353 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1758   [.wsbc 3281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-v 3067  df-sbc 3282
This theorem is referenced by:  sbcabel  3370  csbuni  4214  csbunigOLD  4215  csbxp  5013  csbxpgOLD  5014  sbcfung  5536  f1od2  26155  sbtru  29046  sbfal  29047  fmptsnd  30857  trsbc  31544  csbxpgVD  31927  csbunigVD  31931  bnj89  32007  bnj525  32027  bnj1128  32278  cdlemk40  34864  cdlemkid3N  34880  cdlemkid4  34881
  Copyright terms: Public domain W3C validator