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

Theorem sspss 3275
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 3261 . . . . 5  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
21simplbi2 608 . . . 4  |-  ( A 
C_  B  ->  ( -.  A  =  B  ->  A  C.  B ) )
32con1d 116 . . 3  |-  ( A 
C_  B  ->  ( -.  A  C.  B  ->  A  =  B )
)
43orrd 367 . 2  |-  ( A 
C_  B  ->  ( A  C.  B  \/  A  =  B ) )
5 pssss 3271 . . 3  |-  ( A 
C.  B  ->  A  C_  B )
6 eqimss 3230 . . 3  |-  ( A  =  B  ->  A  C_  B )
75, 6jaoi 368 . 2  |-  ( ( A  C.  B  \/  A  =  B )  ->  A  C_  B )
84, 7impbii 180 1  |-  ( A 
C_  B  <->  ( A  C.  B  \/  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    \/ wo 357    = wceq 1623    C_ wss 3152    C. wpss 3153
This theorem is referenced by:  sspsstri  3278  sspsstr  3281  psssstr  3282  ordsseleq  4421  sorpssuni  6286  sorpssint  6287  ssnnfi  7082  ackbij1b  7865  fin23lem40  7977  zorng  8131  psslinpr  8655  suplem2pr  8677  mrissmrcd  13542  pgpssslw  14925  pgpfac1lem5  15314  idnghm  18252  dfon2lem4  24142  finminlem  26231  lkrss2N  29359  dvh3dim3N  31639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ne 2448  df-in 3159  df-ss 3166  df-pss 3168
  Copyright terms: Public domain W3C validator