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

Theorem sbcg 3390
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3388. (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 1712 . 2  |-  F/ x ph
21sbcgf 3388 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1823   [.wsbc 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3108  df-sbc 3325
This theorem is referenced by:  sbcabel  3402  csbuni  4263  csbxp  5070  sbcfung  5593  fmptsnd  6069  f1od2  27781  sbtru  30751  sbfal  30752  trsbc  33720  csbunigOLD  34035  csbxpgOLD  34037  csbxpgVD  34114  csbunigVD  34118  bnj89  34194  bnj525  34214  bnj1128  34466  cdlemk40  37059  cdlemkid3N  37075  cdlemkid4  37076  frege70  38434  frege77  38441  frege116  38480  frege118  38482
  Copyright terms: Public domain W3C validator