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

Theorem sseq12i 3972
Description: An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
sseq1i.1 𝐴 = 𝐵
sseq12i.2 𝐶 = 𝐷
Assertion
Ref Expression
sseq12i (𝐴𝐶𝐵𝐷)

Proof of Theorem sseq12i
StepHypRef Expression
1 sseq1i.1 . 2 𝐴 = 𝐵
2 sseq12i.2 . 2 𝐶 = 𝐷
3 sseq12 3969 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))
41, 2, 3mp2an 691 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wss 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-in 3915  df-ss 3925
This theorem is referenced by:  3sstr3i  3984  3sstr4i  3985  3sstr3g  3986  3sstr4g  3987  ss2rab  4022  rabsssn  4581  issubgr  27059  pjordi  29954  mdsldmd1i  30112  iuninc  30319  cvmlift2lem12  32635  brtrclfv2  40358  nzss  40955  hoidmvle  43178  ovolval5lem3  43232  fldhmsubc  44647  fldhmsubcALTV  44665
  Copyright terms: Public domain W3C validator