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

Theorem sseq12i 3469
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  |-  A  =  B
sseq12i.2  |-  C  =  D
Assertion
Ref Expression
sseq12i  |-  ( A 
C_  C  <->  B  C_  D
)

Proof of Theorem sseq12i
StepHypRef Expression
1 sseq1i.1 . 2  |-  A  =  B
2 sseq12i.2 . 2  |-  C  =  D
3 sseq12 3466 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  C_  C  <->  B 
C_  D ) )
41, 2, 3mp2an 683 1  |-  ( A 
C_  C  <->  B  C_  D
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    = wceq 1454    C_ wss 3415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3422  df-ss 3429
This theorem is referenced by:  3sstr3i  3481  3sstr4i  3482  3sstr3g  3483  3sstr4g  3484  ss2rab  3516  rabsssn  4013  pjordi  27874  mdsldmd1i  28032  iuninc  28224  cvmlift2lem12  30085  brtrclfv2  36363  nzss  36709  hoidmvle  38459  issubgr  39392  fldhmsubc  40358  fldhmsubcALTV  40377
  Copyright terms: Public domain W3C validator