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

Theorem sspss 3390
Description: Subclass in terms of proper subclass. (Contributed by NM, 25-Feb-1996.)
Assertion
Ref Expression
sspss  |-  ( A 
C_  B  <->  ( A  C.  B  \/  A  =  B ) )

Proof of Theorem sspss
StepHypRef Expression
1 dfpss2 3376 . . . . 5  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
21simplbi2 609 . . . 4  |-  ( A 
C_  B  ->  ( -.  A  =  B  ->  A  C.  B ) )
32con1d 118 . . 3  |-  ( A 
C_  B  ->  ( -.  A  C.  B  ->  A  =  B )
)
43orrd 368 . 2  |-  ( A 
C_  B  ->  ( A  C.  B  \/  A  =  B ) )
5 pssss 3386 . . 3  |-  ( A 
C.  B  ->  A  C_  B )
6 eqimss 3344 . . 3  |-  ( A  =  B  ->  A  C_  B )
75, 6jaoi 369 . 2  |-  ( ( A  C.  B  \/  A  =  B )  ->  A  C_  B )
84, 7impbii 181 1  |-  ( A 
C_  B  <->  ( A  C.  B  \/  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    \/ wo 358    = wceq 1649    C_ wss 3264    C. wpss 3265
This theorem is referenced by:  sspsstri  3393  sspsstr  3396  psssstr  3397  ordsseleq  4552  sorpssuni  6468  sorpssint  6469  ssnnfi  7265  ackbij1b  8053  fin23lem40  8165  zorng  8318  psslinpr  8842  suplem2pr  8864  mrissmrcd  13793  pgpssslw  15176  pgpfac1lem5  15565  idnghm  18649  dfon2lem4  25167  finminlem  26013  lkrss2N  29285  dvh3dim3N  31565
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-ne 2553  df-in 3271  df-ss 3278  df-pss 3280
  Copyright terms: Public domain W3C validator