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

Theorem sbcieg 3346
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 1694 . 2  |-  F/ x ps
2 sbcieg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
31, 2sbciegf 3345 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ph  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383    e. wcel 1804   [.wsbc 3313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097  df-sbc 3314
This theorem is referenced by:  sbcie  3348  ralsng  4049  rexsng  4050  rabsnif  4084  ralrnmpt  6025  fpwwe2lem3  9014  nn1suc  10563  mrcmndind  15871  fgcl  20252  cfinfil  20267  csdfil  20268  supfil  20269  fin1aufil  20306  ifeqeqx  27291  nn0min  27484  2nn0ind  30856  zindbi  30857  trsbcVD  33405  onfrALTlem5VD  33413  bnj1452  33836  cdlemk35s  36397  cdlemk39s  36399  cdlemk42  36401
  Copyright terms: Public domain W3C validator