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

Theorem 3sstr4i 3230
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 3217 . 2  |-  ( C 
C_  D  <->  A  C_  B
)
51, 4mpbir 200 1  |-  C  C_  D
Colors of variables: wff set class
Syntax hints:    = wceq 1632    C_ wss 3165
This theorem is referenced by:  brab2a  4754  rncoss  4961  imassrn  5041  rnin  5106  ssoprab2i  5952  omopthlem2  6670  rankval4  7555  cardf2  7592  r0weon  7656  dcomex  8089  axdc2lem  8090  fpwwe2lem1  8269  canthwe  8289  recmulnq  8604  npex  8626  axresscn  8786  odlem1  14866  gexlem1  14906  psrbagsn  16252  2ndcctbss  17197  uniioombllem4  18957  uniioombllem5  18958  eff1olem  19926  birthdaylem1  20262  nvss  21165  lediri  22132  lejdiri  22134  sshhococi  22141  mayetes3i  22325  kur14lem6  23757  cvmlift2lem12  23860  bpoly4  24866  posprsr  25343  inposet  25381  0alg  25859  uvcff  27343  relopabVD  28993  lclkrs2  32352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator