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

Theorem sseq12i 3825
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 3822 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))
41, 2, 3mp2an 684 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 198   = wceq 1653  wss 3767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781
This theorem is referenced by:  3sstr3i  3837  3sstr4i  3838  3sstr3g  3839  3sstr4g  3840  ss2rab  3872  rabsssn  4404  issubgr  26497  pjordi  29549  mdsldmd1i  29707  iuninc  29888  cvmlift2lem12  31805  brtrclfv2  38790  nzss  39286  hoidmvle  41548  ovolval5lem3  41602  fldhmsubc  42871  fldhmsubcALTV  42889
  Copyright terms: Public domain W3C validator