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

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

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 1875 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
2 dfsbcq2 3007 . 2  |-  ( x  =  A  ->  ( [ x  /  x ] ph  <->  [. A  /  x ]. ph ) )
31, 2syl5bbr 250 1  |-  ( x  =  A  ->  ( ph 
<-> 
[. A  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   [wsb 1638   [.wsbc 3004
This theorem is referenced by:  sbceq2a  3015  elrabsf  3042  cbvralcsf  3156  euotd  4283  tfindes  4669  ralrnmpt  5685  sbcopeq1a  6188  riotass2  6348  riotass  6349  riotasv2s  6367  findcard2  7114  ac6sfi  7117  indexfi  7179  uzindOLD  10122  nn0ind-raph  10128  fzrevral  10882  wrdind  11493  prmind2  12785  elmptrab  17538  isfildlem  17568  ifeqeqx  23050  setinds  24205  dfon2lem1  24210  tfisg  24275  wfisg  24280  frinsg  24316  indexdom  26516  sdclem2  26555  sdclem1  26556  fdc  26558  fdc1  26559  sbccomieg  26973  rexrabdioph  26978  rexfrabdioph  26979  aomclem6  27259  pm13.13a  27710  pm13.13b  27711  pm13.14  27712  mpt2xopoveq  28201  tratrb  28598  bnj919  29113  bnj976  29125  bnj1468  29194  bnj110  29206  bnj150  29224  bnj151  29225  bnj607  29264  bnj873  29272  bnj849  29273  bnj1388  29379
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-sbc 3005
  Copyright terms: Public domain W3C validator