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

Theorem sbcie 3197
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.)
Hypotheses
Ref Expression
sbcie.1  |-  A  e. 
_V
sbcie.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
sbcie  |-  ( [. A  /  x ]. ph  <->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem sbcie
StepHypRef Expression
1 sbcie.1 . 2  |-  A  e. 
_V
2 sbcie.2 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32sbcieg 3195 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  ps ) )
41, 3ax-mp 5 1  |-  ( [. A  /  x ]. ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726   _Vcvv 2958   [.wsbc 3163
This theorem is referenced by:  tfinds2  4846  findcard2  7351  ac6sfi  7354  ac6num  8364  fpwwe  8526  nn1suc  10026  wrdind  11796  cjth  11913  prmind2  13095  joinlem  14452  meetlem  14459  isghm  15011  islmod  15959  fgcl  17915  cfinfil  17930  csdfil  17931  supfil  17932  fin1aufil  17969  quotval  20214  fprodser  25280  soseq  25534  sdclem2  26460  fdc  26463  fdc1  26464  rabren3dioph  26890  2nn0ind  27022  zindbi  27023  islindf  27273  bnj62  29159  bnj610  29189  bnj976  29222  bnj106  29313  bnj125  29317  bnj154  29323  bnj155  29324  bnj526  29333  bnj540  29337  bnj591  29356  bnj609  29362  bnj893  29373  bnj1417  29484  lshpkrlem3  29984  hdmap1fval  32669  hdmapfval  32702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-sbc 3164
  Copyright terms: Public domain W3C validator