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

Theorem 3sstr4i 4025
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 4012 . 2 (𝐶𝐷𝐴𝐵)
51, 4mpbir 230 1 𝐶𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  wss 3949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-in 3956  df-ss 3966
This theorem is referenced by:  relopabiv  5826  rncoss  5979  imassrn  6079  rnin  6156  inimass  6164  f1ossf1o  7143  ssoprab2i  7537  omopthlem2  8687  1sdom2dom  9278  rankval4  9898  cardf2  9974  r0weon  10043  dcomex  10478  axdc2lem  10479  fpwwe2lem1  10662  canthwe  10682  recmulnq  10995  npex  11017  axresscn  11179  mpoaddf  11240  mpomulf  11241  trclublem  14982  bpoly4  16043  2strop1  17215  odlem1  19497  gexlem1  19541  pzriprnglem4  21417  psrbagsn  22014  bwth  23334  2ndcctbss  23379  uniioombllem4  25535  uniioombllem5  25536  eff1olem  26502  birthdaylem1  26903  nvss  30423  lediri  31367  lejdiri  31369  sshhococi  31376  mayetes3i  31559  disjxpin  32399  imadifxp  32412  sxbrsigalem5  33941  eulerpartlemmf  34028  kur14lem6  34854  cvmlift2lem12  34957  bj-xpcossxp  36701  bj-rrhatsscchat  36748  mblfinlem4  37166  lclkrs2  41045  areaquad  42675  corclrcl  43168  corcltrcl  43200  relopabVD  44371  ovolval5lem3  46071
  Copyright terms: Public domain W3C validator