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

Theorem sbceq1a 3163
Description: Equality theorem for class substitution. Class version of sbequ12 1944. (Contributed by NM, 26-Sep-2003.)
Assertion
Ref Expression
sbceq1a  |-  ( x  =  A  ->  ( ph 
<-> 
[. A  /  x ]. ph ) )

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 1947 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
2 dfsbcq2 3156 . 2  |-  ( x  =  A  ->  ( [ x  /  x ] ph  <->  [. A  /  x ]. ph ) )
31, 2syl5bbr 251 1  |-  ( x  =  A  ->  ( ph 
<-> 
[. A  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   [wsb 1658   [.wsbc 3153
This theorem is referenced by:  sbceq2a  3164  elrabsf  3191  cbvralcsf  3303  euotd  4449  tfindes  4834  ralrnmpt  5870  sbcopeq1a  6391  mpt2xopoveq  6462  riotass2  6569  riotass  6570  riotasv2s  6588  findcard2  7340  ac6sfi  7343  indexfi  7406  uzindOLD  10356  nn0ind-raph  10362  fzrevral  11123  wrdind  11783  prmind2  13082  elmptrab  17851  isfildlem  17881  ifeqeqx  23993  setinds  25397  dfon2lem1  25402  tfisg  25471  wfisg  25476  frinsg  25512  indexdom  26427  sdclem2  26437  sdclem1  26438  fdc1  26441  sbccomieg  26840  rexrabdioph  26845  rexfrabdioph  26846  aomclem6  27125  pm13.13a  27575  pm13.13b  27576  pm13.14  27577  tratrb  28557  bnj919  29073  bnj976  29085  bnj1468  29154  bnj110  29166  bnj150  29184  bnj151  29185  bnj607  29224  bnj873  29232  bnj849  29233  bnj1388  29339
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-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-sbc 3154
  Copyright terms: Public domain W3C validator