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

Theorem sbcie 3101
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 3099 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  ps ) )
41, 3ax-mp 8 1  |-  ( [. A  /  x ]. ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642    e. wcel 1710   _Vcvv 2864   [.wsbc 3067
This theorem is referenced by:  tfinds2  4736  findcard2  7188  ac6sfi  7191  ac6num  8196  fpwwe  8358  nn1suc  9857  wrdind  11573  cjth  11684  prmind2  12866  joinlem  14223  meetlem  14230  isghm  14782  islmod  15730  fgcl  17675  cfinfil  17690  csdfil  17691  supfil  17692  fin1aufil  17729  quotval  19776  fprodser  24576  soseq  24812  sdclem2  25776  fdc  25779  fdc1  25780  rabren3dioph  26221  2nn0ind  26353  zindbi  26354  islindf  26605  bnj62  28508  bnj610  28538  bnj976  28571  bnj106  28662  bnj125  28666  bnj154  28672  bnj155  28673  bnj526  28682  bnj540  28686  bnj591  28705  bnj609  28711  bnj893  28722  bnj1417  28833  lshpkrlem3  29371  hdmap1fval  32056  hdmapfval  32089
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-sbc 3068
  Copyright terms: Public domain W3C validator