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

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

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 1948 . 2  |-  ( [ x  /  x ] ph 
<-> 
ph )
2 dfsbcq2 3166 . 2  |-  ( x  =  A  ->  ( [ x  /  x ] ph  <->  [. A  /  x ]. ph ) )
31, 2syl5bbr 252 1  |-  ( x  =  A  ->  ( ph 
<-> 
[. A  /  x ]. ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   [wsb 1659   [.wsbc 3163
This theorem is referenced by:  sbceq2a  3174  elrabsf  3201  cbvralcsf  3313  euotd  4460  tfindes  4845  ralrnmpt  5881  sbcopeq1a  6402  mpt2xopoveq  6473  riotass2  6580  riotass  6581  riotasv2s  6599  findcard2  7351  ac6sfi  7354  indexfi  7417  uzindOLD  10369  nn0ind-raph  10375  fzrevral  11136  wrdind  11796  prmind2  13095  elmptrab  17864  isfildlem  17894  ifeqeqx  24006  setinds  25410  dfon2lem1  25415  tfisg  25484  wfisg  25489  frinsg  25525  indexdom  26450  sdclem2  26460  sdclem1  26461  fdc1  26464  sbccomieg  26863  rexrabdioph  26868  rexfrabdioph  26869  aomclem6  27148  pm13.13a  27598  pm13.13b  27599  pm13.14  27600  oprabv  28103  elovmpt2rab  28104  elovmpt2rab1  28105  ovmpt3rab1  28106  elovmpt3rab1  28107  tratrb  28694  bnj919  29210  bnj976  29222  bnj1468  29291  bnj110  29303  bnj150  29321  bnj151  29322  bnj607  29361  bnj873  29369  bnj849  29370  bnj1388  29476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-sbc 3164
  Copyright terms: Public domain W3C validator