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

Theorem 3sstr4i 3217
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 3204 . 2  |-  ( C 
C_  D  <->  A  C_  B
)
51, 4mpbir 200 1  |-  C  C_  D
Colors of variables: wff set class
Syntax hints:    = wceq 1623    C_ wss 3152
This theorem is referenced by:  brab2a  4738  rncoss  4945  imassrn  5025  rnin  5090  ssoprab2i  5936  omopthlem2  6654  rankval4  7539  cardf2  7576  r0weon  7640  dcomex  8073  axdc2lem  8074  fpwwe2lem1  8253  canthwe  8273  recmulnq  8588  npex  8610  axresscn  8770  odlem1  14850  gexlem1  14890  psrbagsn  16236  2ndcctbss  17181  uniioombllem4  18941  uniioombllem5  18942  eff1olem  19910  birthdaylem1  20246  nvss  21149  lediri  22116  lejdiri  22118  sshhococi  22125  mayetes3i  22309  kur14lem6  23742  cvmlift2lem12  23845  bpoly4  24794  posprsr  25240  inposet  25278  0alg  25756  uvcff  27240  relopabVD  28677  lclkrs2  31730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator