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

Theorem 3sstr4i 3607
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 3594 . 2 (𝐶𝐷𝐴𝐵)
51, 4mpbir 220 1 𝐶𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  brab2a  5091  rncoss  5307  imassrn  5396  rnin  5461  inimass  5468  ssoprab2i  6647  omopthlem2  7623  rankval4  8613  cardf2  8652  r0weon  8718  dcomex  9152  axdc2lem  9153  fpwwe2lem1  9332  canthwe  9352  recmulnq  9665  npex  9687  axresscn  9848  trclublem  13582  bpoly4  14629  2strop1  15814  odlem1  17777  gexlem1  17817  psrbagsn  19316  bwth  21023  2ndcctbss  21068  uniioombllem4  23160  uniioombllem5  23161  eff1olem  24098  birthdaylem1  24478  nvss  26832  lediri  27780  lejdiri  27782  sshhococi  27789  mayetes3i  27972  disjxpin  28783  imadifxp  28796  sxbrsigalem5  29677  eulerpartlemmf  29764  kur14lem6  30447  cvmlift2lem12  30550  bj-rrhatsscchat  32300  mblfinlem4  32619  lclkrs2  35847  areaquad  36821  corclrcl  37018  corcltrcl  37050  relopabVD  38159
  Copyright terms: Public domain W3C validator