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

Theorem 3sstr4i 4007
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 3994 . 2 (𝐶𝐷𝐴𝐵)
51, 4mpbir 232 1 𝐶𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  relopabiv  5686  rncoss  5836  imassrn  5933  rnin  5998  inimass  6005  f1ossf1o  6882  ssoprab2i  7252  omopthlem2  8272  rankval4  9284  cardf2  9360  r0weon  9426  dcomex  9857  axdc2lem  9858  fpwwe2lem1  10041  canthwe  10061  recmulnq  10374  npex  10396  axresscn  10558  trclublem  14343  bpoly4  15401  2strop1  16595  odlem1  18592  gexlem1  18633  psrbagsn  20203  bwth  21946  2ndcctbss  21991  uniioombllem4  24114  uniioombllem5  24115  eff1olem  25059  birthdaylem1  25456  nvss  28297  lediri  29241  lejdiri  29243  sshhococi  29250  mayetes3i  29433  disjxpin  30266  imadifxp  30279  sxbrsigalem5  31445  eulerpartlemmf  31532  kur14lem6  32355  cvmlift2lem12  32458  bj-rrhatsscchat  34410  mblfinlem4  34813  lclkrs2  38556  areaquad  39701  corclrcl  39930  corcltrcl  39962  relopabVD  41112
  Copyright terms: Public domain W3C validator