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

Theorem sbcie 3025
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 3023 . 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 1623    e. wcel 1684   _Vcvv 2788   [.wsbc 2991
This theorem is referenced by:  tfinds2  4654  findcard2  7098  ac6sfi  7101  ac6num  8106  fpwwe  8268  nn1suc  9767  wrdind  11477  cjth  11588  prmind2  12769  joinlem  14124  meetlem  14131  isghm  14683  islmod  15631  fgcl  17573  cfinfil  17588  csdfil  17589  supfil  17590  fin1aufil  17627  quotval  19672  soseq  24254  isconcl5a  26101  isconcl5ab  26102  isibg2  26110  isibcg  26191  sdclem2  26452  fdc  26455  fdc1  26456  rabren3dioph  26898  2nn0ind  27030  zindbi  27031  islindf  27282  bnj62  28746  bnj610  28776  bnj976  28809  bnj106  28900  bnj125  28904  bnj154  28910  bnj155  28911  bnj526  28920  bnj540  28924  bnj591  28943  bnj609  28949  bnj893  28960  bnj1417  29071  lshpkrlem3  29302  hdmap1fval  31987  hdmapfval  32020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sbc 2992
  Copyright terms: Public domain W3C validator