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

Theorem sbcieg 3311
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 1771 . 2  |-  F/ x ps
2 sbcieg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2sbciegf 3310 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1454    e. wcel 1897   [.wsbc 3278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-v 3058  df-sbc 3279
This theorem is referenced by:  sbcie  3313  ralsng  4017  rexsng  4018  rabsnif  4053  ralrnmpt  6053  fpwwe2lem3  9083  nn1suc  10657  mrcmndind  16661  fgcl  20941  cfinfil  20956  csdfil  20957  supfil  20958  fin1aufil  20995  ifeqeqx  28206  nn0min  28432  bnj1452  29909  cdlemk35s  34548  cdlemk39s  34550  cdlemk42  34552  2nn0ind  35837  zindbi  35838  trsbcVD  37313  onfrALTlem5VD  37321
  Copyright terms: Public domain W3C validator