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

Theorem 3sstr4i 3503
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 3490 . 2  |-  ( C 
C_  D  <->  A  C_  B
)
51, 4mpbir 212 1  |-  C  C_  D
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  brab2a  4903  rncoss  5114  imassrn  5198  rnin  5264  inimass  5271  ssoprab2i  6400  omopthlem2  7369  rankval4  8347  cardf2  8386  r0weon  8452  dcomex  8885  axdc2lem  8886  fpwwe2lem1  9064  canthwe  9084  recmulnq  9397  npex  9419  axresscn  9580  trclublem  13060  bpoly4  14112  2strop1  15235  odlem1  17181  odlem1OLD  17184  gexlem1  17228  gexlem1OLD  17230  psrbagsn  18718  bwth  20424  2ndcctbss  20469  uniioombllem4  22543  uniioombllem5  22544  eff1olem  23496  birthdaylem1  23876  nvss  26211  lediri  27189  lejdiri  27191  sshhococi  27198  mayetes3i  27381  disjxpin  28201  imadifxp  28215  sxbrsigalem5  29119  eulerpartlemmf  29217  kur14lem6  29943  cvmlift2lem12  30046  bj-rrhatsscchat  31643  mblfinlem4  31945  lclkrs2  35078  areaquad  36072  corclrcl  36270  corcltrcl  36302  relopabVD  37272
  Copyright terms: Public domain W3C validator