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

Theorem sseq12i 3594
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 3591 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐶𝐵𝐷))
41, 2, 3mp2an 704 1 (𝐴𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = 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:  3sstr3i  3606  3sstr4i  3607  3sstr3g  3608  3sstr4g  3609  ss2rab  3641  rabsssn  4162  pjordi  28416  mdsldmd1i  28574  iuninc  28761  cvmlift2lem12  30550  brtrclfv2  37038  nzss  37538  hoidmvle  39490  ovolval5lem3  39544  issubgr  40495  fldhmsubc  41876  fldhmsubcALTV  41895
  Copyright terms: Public domain W3C validator