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

Theorem sbceq1a 3171
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 3164 . 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 3161
This theorem is referenced by:  sbceq2a  3172  elrabsf  3199  cbvralcsf  3311  euotd  4457  tfindes  4842  ralrnmpt  5878  sbcopeq1a  6399  mpt2xopoveq  6470  riotass2  6577  riotass  6578  riotasv2s  6596  findcard2  7348  ac6sfi  7351  indexfi  7414  uzindOLD  10364  nn0ind-raph  10370  fzrevral  11131  wrdind  11791  prmind2  13090  elmptrab  17859  isfildlem  17889  ifeqeqx  24001  setinds  25405  dfon2lem1  25410  tfisg  25479  wfisg  25484  frinsg  25520  indexdom  26436  sdclem2  26446  sdclem1  26447  fdc1  26450  sbccomieg  26849  rexrabdioph  26854  rexfrabdioph  26855  aomclem6  27134  pm13.13a  27584  pm13.13b  27585  pm13.14  27586  oprabv  28085  tratrb  28620  bnj919  29136  bnj976  29148  bnj1468  29217  bnj110  29229  bnj150  29247  bnj151  29248  bnj607  29287  bnj873  29295  bnj849  29296  bnj1388  29402
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 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-sbc 3162
  Copyright terms: Public domain W3C validator