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

Theorem sbcieg 3207
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 1672 . 2  |-  F/ x ps
2 sbcieg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2sbciegf 3206 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362    e. wcel 1755   [.wsbc 3175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-v 2964  df-sbc 3176
This theorem is referenced by:  sbcie  3209  ralsng  3900  rexsng  3901  rabsnif  3932  ralrnmpt  5840  fpwwe2lem3  8788  nn1suc  10331  mrcmndind  15476  fgcl  19293  cfinfil  19308  csdfil  19309  supfil  19310  fin1aufil  19347  ifeqeqx  25726  nn0min  25913  2nn0ind  29131  zindbi  29132  trsbcVD  31315  onfrALTlem5VD  31323  bnj1452  31745  cdlemk35s  34154  cdlemk39s  34156  cdlemk42  34158
  Copyright terms: Public domain W3C validator