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

Theorem 3sstr4i 3992
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 3979 . 2 (𝐶𝐷𝐴𝐵)
51, 4mpbir 230 1 𝐶𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  relopabiv  5781  rncoss  5932  imassrn  6029  rnin  6104  inimass  6112  f1ossf1o  7079  ssoprab2i  7472  omopthlem2  8611  1sdom2dom  9198  rankval4  9810  cardf2  9886  r0weon  9955  dcomex  10390  axdc2lem  10391  fpwwe2lem1  10574  canthwe  10594  recmulnq  10907  npex  10929  axresscn  11091  trclublem  14887  bpoly4  15949  2strop1  17118  odlem1  19324  gexlem1  19368  psrbagsn  21487  bwth  22777  2ndcctbss  22822  uniioombllem4  24966  uniioombllem5  24967  eff1olem  25920  birthdaylem1  26317  nvss  29577  lediri  30521  lejdiri  30523  sshhococi  30530  mayetes3i  30713  disjxpin  31548  imadifxp  31561  sxbrsigalem5  32928  eulerpartlemmf  33015  kur14lem6  33845  cvmlift2lem12  33948  bj-xpcossxp  35689  bj-rrhatsscchat  35736  mblfinlem4  36147  lclkrs2  40032  areaquad  41579  corclrcl  42053  corcltrcl  42085  relopabVD  43257  ovolval5lem3  44969
  Copyright terms: Public domain W3C validator