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

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

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 1863 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
2 dfsbcq2 2994 . 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 1623   [wsb 1629   [.wsbc 2991
This theorem is referenced by:  sbceq2a  3002  elrabsf  3029  cbvralcsf  3143  euotd  4267  tfindes  4653  ralrnmpt  5669  sbcopeq1a  6172  riotass2  6332  riotass  6333  riotasv2s  6351  findcard2  7098  ac6sfi  7101  indexfi  7163  uzindOLD  10106  nn0ind-raph  10112  fzrevral  10866  wrdind  11477  prmind2  12769  elmptrab  17522  isfildlem  17552  ifeqeqx  23034  setinds  24134  dfon2lem1  24139  tfisg  24204  wfisg  24209  frinsg  24245  indexdom  26413  sdclem2  26452  sdclem1  26453  fdc  26455  fdc1  26456  sbccomieg  26870  rexrabdioph  26875  rexfrabdioph  26876  aomclem6  27156  pm13.13a  27607  pm13.13b  27608  pm13.14  27609  mpt2xopoveq  28085  tratrb  28299  bnj919  28797  bnj976  28809  bnj1468  28878  bnj110  28890  bnj150  28908  bnj151  28909  bnj607  28948  bnj873  28956  bnj849  28957  bnj1388  29063
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-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-sbc 2992
  Copyright terms: Public domain W3C validator