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

Theorem 3sstr4i 3958
 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 𝐴𝐵
3sstr4.2 𝐶 = 𝐴
3sstr4.3 𝐷 = 𝐵
Assertion
Ref Expression
3sstr4i 𝐶𝐷

Proof of Theorem 3sstr4i
StepHypRef Expression
1 3sstr4.1 . 2 𝐴𝐵
2 3sstr4.2 . . 3 𝐶 = 𝐴
3 3sstr4.3 . . 3 𝐷 = 𝐵
42, 3sseq12i 3945 . 2 (𝐶𝐷𝐴𝐵)
51, 4mpbir 234 1 𝐶𝐷
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ⊆ wss 3881 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898 This theorem is referenced by:  relopabiv  5658  rncoss  5809  imassrn  5908  rnin  5973  inimass  5980  f1ossf1o  6868  ssoprab2i  7243  omopthlem2  8269  rankval4  9283  cardf2  9359  r0weon  9426  dcomex  9861  axdc2lem  9862  fpwwe2lem1  10045  canthwe  10065  recmulnq  10378  npex  10400  axresscn  10562  trclublem  14349  bpoly4  15408  2strop1  16602  odlem1  18659  gexlem1  18700  psrbagsn  20740  bwth  22025  2ndcctbss  22070  uniioombllem4  24200  uniioombllem5  24201  eff1olem  25150  birthdaylem1  25547  nvss  28386  lediri  29330  lejdiri  29332  sshhococi  29339  mayetes3i  29522  disjxpin  30361  imadifxp  30374  sxbrsigalem5  31671  eulerpartlemmf  31758  kur14lem6  32586  cvmlift2lem12  32689  bj-xpcossxp  34623  bj-rrhatsscchat  34670  mblfinlem4  35116  lclkrs2  38855  areaquad  40209  corclrcl  40451  corcltrcl  40483  relopabVD  41650
 Copyright terms: Public domain W3C validator