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

Theorem sbcieg 3036
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.)
Hypothesis
Ref Expression
sbcieg.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
sbcieg  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
Distinct variable groups:    x, A    ps, x
Allowed substitution hints:    ph( x)    V( x)

Proof of Theorem sbcieg
StepHypRef Expression
1 elex 2809 . 2  |-  ( A  e.  V  ->  A  e.  _V )
2 nfv 1609 . . 3  |-  F/ x ps
3 sbcieg.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
42, 3sbciegf 3035 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  ps ) )
51, 4syl 15 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696   _Vcvv 2801   [.wsbc 3004
This theorem is referenced by:  sbcie  3038  ralsng  3685  rexsng  3686  ralrnmpt  5685  fpwwe2lem3  8271  nn1suc  9783  fgcl  17589  cfinfil  17604  csdfil  17605  supfil  17606  fin1aufil  17643  ifeqeqx  23050  2nn0ind  27133  zindbi  27134  trsbc  28603  onfrALTlem5  28606  trsbcVD  28969  onfrALTlem5VD  28977  bnj1452  29398  cdlemk35s  31748  cdlemk39s  31750  cdlemk42  31752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sbc 3005
  Copyright terms: Public domain W3C validator