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

Theorem 3sstr4i 3506
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 3493 . 2  |-  ( C 
C_  D  <->  A  C_  B
)
51, 4mpbir 209 1  |-  C  C_  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    C_ wss 3439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3446  df-ss 3453
This theorem is referenced by:  brab2a  4999  rncoss  5211  imassrn  5291  rnin  5357  inimass  5364  ssoprab2i  6292  omopthlem2  7208  rankval4  8188  cardf2  8227  r0weon  8293  dcomex  8730  axdc2lem  8731  fpwwe2lem1  8912  canthwe  8932  recmulnq  9247  npex  9269  axresscn  9429  odlem1  16162  gexlem1  16202  psrbagsn  17704  bwth  19148  2ndcctbss  19194  uniioombllem4  21202  uniioombllem5  21203  eff1olem  22140  birthdaylem1  22481  nvss  24143  lediri  25112  lejdiri  25114  sshhococi  25121  mayetes3i  25305  disjxpin  26101  imadifxp  26110  sxbrsigalem5  26867  eulerpartlemmf  26922  kur14lem6  27263  cvmlift2lem12  27367  bpoly4  28366  mblfinlem4  28599  areaquad  29760  relopabVD  31989  bj-rrhatsscchat  32917  lclkrs2  35543
  Copyright terms: Public domain W3C validator