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

Theorem sbcieg 3327
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 nfv 1674 . 2  |-  F/ x ps
2 sbcieg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2sbciegf 3326 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1370    e. wcel 1758   [.wsbc 3294
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 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3080  df-sbc 3295
This theorem is referenced by:  sbcie  3329  ralsng  4023  rexsng  4024  rabsnif  4055  ralrnmpt  5964  fpwwe2lem3  8915  nn1suc  10458  mrcmndind  15617  fgcl  19593  cfinfil  19608  csdfil  19609  supfil  19610  fin1aufil  19647  ifeqeqx  26081  nn0min  26262  2nn0ind  29457  zindbi  29458  trsbcVD  31968  onfrALTlem5VD  31976  bnj1452  32398  cdlemk35s  34944  cdlemk39s  34946  cdlemk42  34948
  Copyright terms: Public domain W3C validator