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

Theorem 3sstr4i 3379
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 3366 . 2  |-  ( C 
C_  D  <->  A  C_  B
)
51, 4mpbir 201 1  |-  C  C_  D
Colors of variables: wff set class
Syntax hints:    = wceq 1652    C_ wss 3312
This theorem is referenced by:  brab2a  4919  rncoss  5128  imassrn  5208  rnin  5273  inimass  5280  ssoprab2i  6154  omopthlem2  6891  rankval4  7783  cardf2  7820  r0weon  7884  dcomex  8317  axdc2lem  8318  fpwwe2lem1  8496  canthwe  8516  recmulnq  8831  npex  8853  axresscn  9013  odlem1  15163  gexlem1  15203  psrbagsn  16545  2ndcctbss  17508  uniioombllem4  19468  uniioombllem5  19469  eff1olem  20440  birthdaylem1  20780  nvss  22062  lediri  23029  lejdiri  23031  sshhococi  23038  mayetes3i  23222  disjxpin  24018  imadifxp  24028  sxbrsigalem5  24628  kur14lem6  24887  cvmlift2lem12  24991  bpoly4  26070  mblfinlem3  26209  uvcff  27172  relopabVD  28914  lclkrs2  32239
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator