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

Theorem sbceq1d 3329
Description: Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.)
Hypothesis
Ref Expression
sbceq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sbceq1d  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. B  /  x ]. ps ) )

Proof of Theorem sbceq1d
StepHypRef Expression
1 sbceq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 dfsbcq 3326 . 2  |-  ( A  =  B  ->  ( [. A  /  x ]. ps  <->  [. B  /  x ]. ps ) )
31, 2syl 16 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. B  /  x ]. ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398   [.wsbc 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-cleq 2446  df-clel 2449  df-sbc 3325
This theorem is referenced by:  sbceq1dd  3330  sbcnestgf  3834  ralrnmpt  6016  tfindes  6670  findes  6703  findcard2  7752  ac6sfi  7756  indexfi  7820  ac6num  8850  nn1suc  10552  uzind4s  11142  uzind4s2  11143  fzrevral  11767  fzshftral  11770  wrdind  12693  wrd2ind  12694  cjth  13018  prmind2  14312  isprs  15758  isdrs  15762  joinlem  15840  meetlem  15854  istos  15864  isdlat  16022  gsumvalx  16096  mrcmndind  16196  issrg  17354  islmod  17711  quotval  22854  nn0min  27845  sdclem2  30475  fdc  30478  rexrabdioph  30967  2nn0ind  31120  zindbi  31121  iotasbcq  31585  bnj944  34397  hdmap1ffval  37920  hdmap1fval  37921
  Copyright terms: Public domain W3C validator