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

Theorem 3sstr4i 3332
Description: Substitution of equality in both sides of a subclass relationship. (Contributed by NM, 13-Jan-1996.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
3sstr4.1  |-  A  C_  B
3sstr4.2  |-  C  =  A
3sstr4.3  |-  D  =  B
Assertion
Ref Expression
3sstr4i  |-  C  C_  D

Proof of Theorem 3sstr4i
StepHypRef Expression
1 3sstr4.1 . 2  |-  A  C_  B
2 3sstr4.2 . . 3  |-  C  =  A
3 3sstr4.3 . . 3  |-  D  =  B
42, 3sseq12i 3319 . 2  |-  ( C 
C_  D  <->  A  C_  B
)
51, 4mpbir 201 1  |-  C  C_  D
Colors of variables: wff set class
Syntax hints:    = wceq 1649    C_ wss 3265
This theorem is referenced by:  brab2a  4869  rncoss  5078  imassrn  5158  rnin  5223  inimass  5230  ssoprab2i  6103  omopthlem2  6837  rankval4  7728  cardf2  7765  r0weon  7829  dcomex  8262  axdc2lem  8263  fpwwe2lem1  8441  canthwe  8461  recmulnq  8776  npex  8798  axresscn  8958  odlem1  15102  gexlem1  15142  psrbagsn  16484  2ndcctbss  17441  uniioombllem4  19347  uniioombllem5  19348  eff1olem  20319  birthdaylem1  20659  nvss  21922  lediri  22889  lejdiri  22891  sshhococi  22898  mayetes3i  23082  imadifxp  23883  sxbrsigalem5  24434  kur14lem6  24678  cvmlift2lem12  24782  bpoly4  25821  uvcff  26911  relopabVD  28356  lclkrs2  31657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-in 3272  df-ss 3279
  Copyright terms: Public domain W3C validator