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

Theorem sbceqbid 3331
Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.)
Hypotheses
Ref Expression
sbceqbid.1  |-  ( ph  ->  A  =  B )
sbceqbid.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
sbceqbid  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. B  /  x ]. ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)    B( x)

Proof of Theorem sbceqbid
StepHypRef Expression
1 sbceqbid.1 . . 3  |-  ( ph  ->  A  =  B )
2 sbceqbid.2 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
32abbidv 2590 . . 3  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
41, 3eleq12d 2536 . 2  |-  ( ph  ->  ( A  e.  {
x  |  ps }  <->  B  e.  { x  |  ch } ) )
5 df-sbc 3325 . 2  |-  ( [. A  /  x ]. ps  <->  A  e.  { x  |  ps } )
6 df-sbc 3325 . 2  |-  ( [. B  /  x ]. ch  <->  B  e.  { x  |  ch } )
74, 5, 63bitr4g 288 1  |-  ( ph  ->  ( [. A  /  x ]. ps  <->  [. B  /  x ]. ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398    e. wcel 1823   {cab 2439   [.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-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3325
This theorem is referenced by:  fpwwe2cbv  8997  fpwwe2lem2  8999  fpwwe2lem3  9000  isprs  15758  isdrs  15762  istos  15864  isdlat  16022  issrg  17354  islmod  17711  fdc  30478  sbccomieg  30966  rexrabdioph  30967  hdmap1ffval  37920  hdmap1fval  37921  hdmapffval  37953  hdmapfval  37954  hgmapffval  38012  hgmapfval  38013
  Copyright terms: Public domain W3C validator