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

Theorem sspss 3608
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 3594 . . . . 5  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
21simplbi2 625 . . . 4  |-  ( A 
C_  B  ->  ( -.  A  =  B  ->  A  C.  B )
)
32con1d 124 . . 3  |-  ( A 
C_  B  ->  ( -.  A  C.  B  ->  A  =  B )
)
43orrd 378 . 2  |-  ( A 
C_  B  ->  ( A  C.  B  \/  A  =  B ) )
5 pssss 3604 . . 3  |-  ( A 
C.  B  ->  A  C_  B )
6 eqimss 3561 . . 3  |-  ( A  =  B  ->  A  C_  B )
75, 6jaoi 379 . 2  |-  ( ( A  C.  B  \/  A  =  B )  ->  A  C_  B )
84, 7impbii 188 1  |-  ( A 
C_  B  <->  ( A  C.  B  \/  A  =  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    \/ wo 368    = wceq 1379    C_ wss 3481    C. wpss 3482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ne 2664  df-in 3488  df-ss 3495  df-pss 3497
This theorem is referenced by:  sspsstri  3611  sspsstr  3614  psssstr  3615  ordsseleq  4913  sorpssuni  6584  sorpssint  6585  ssnnfi  7751  ackbij1b  8631  fin23lem40  8743  zorng  8896  psslinpr  9421  suplem2pr  9443  mrissmrcd  14912  pgpssslw  16507  pgpfac1lem5  17002  idnghm  21118  dfon2lem4  29145  finminlem  30063  lkrss2N  34367  dvh3dim3N  36647
  Copyright terms: Public domain W3C validator