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

Theorem 3sstr4i 3937
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 3924 . 2 (𝐶𝐷𝐴𝐵)
51, 4mpbir 232 1 𝐶𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1525  wss 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-in 3872  df-ss 3880
This theorem is referenced by:  relopabiv  5586  rncoss  5731  imassrn  5824  rnin  5888  inimass  5895  f1ossf1o  6760  ssoprab2i  7126  omopthlem2  8140  rankval4  9149  cardf2  9225  r0weon  9291  dcomex  9722  axdc2lem  9723  fpwwe2lem1  9906  canthwe  9926  recmulnq  10239  npex  10261  axresscn  10423  trclublem  14193  bpoly4  15250  2strop1  16440  odlem1  18398  gexlem1  18438  psrbagsn  19966  bwth  21706  2ndcctbss  21751  uniioombllem4  23874  uniioombllem5  23875  eff1olem  24817  birthdaylem1  25215  nvss  28057  lediri  29001  lejdiri  29003  sshhococi  29010  mayetes3i  29193  disjxpin  30024  imadifxp  30037  sxbrsigalem5  31159  eulerpartlemmf  31246  kur14lem6  32068  cvmlift2lem12  32171  bj-rrhatsscchat  34097  mblfinlem4  34484  lclkrs2  38228  areaquad  39329  corclrcl  39558  corcltrcl  39590  relopabVD  40795
  Copyright terms: Public domain W3C validator