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

Theorem sbcie 3187
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 3185 . 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 177    = wceq 1652    e. wcel 1725   _Vcvv 2948   [.wsbc 3153
This theorem is referenced by:  tfinds2  4835  findcard2  7340  ac6sfi  7343  ac6num  8351  fpwwe  8513  nn1suc  10013  wrdind  11783  cjth  11900  prmind2  13082  joinlem  14439  meetlem  14446  isghm  14998  islmod  15946  fgcl  17902  cfinfil  17917  csdfil  17918  supfil  17919  fin1aufil  17956  quotval  20201  fprodser  25267  soseq  25521  sdclem2  26437  fdc  26440  fdc1  26441  rabren3dioph  26867  2nn0ind  26999  zindbi  27000  islindf  27250  bnj62  29022  bnj610  29052  bnj976  29085  bnj106  29176  bnj125  29180  bnj154  29186  bnj155  29187  bnj526  29196  bnj540  29200  bnj591  29219  bnj609  29225  bnj893  29236  bnj1417  29347  lshpkrlem3  29847  hdmap1fval  32532  hdmapfval  32565
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-sbc 3154
  Copyright terms: Public domain W3C validator