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

Theorem dfpss3 3425
Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
dfpss3  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  B  C_  A ) )

Proof of Theorem dfpss3
StepHypRef Expression
1 dfpss2 3424 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
2 eqss 3355 . . . . 5  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
32baib 872 . . . 4  |-  ( A 
C_  B  ->  ( A  =  B  <->  B  C_  A
) )
43notbid 286 . . 3  |-  ( A 
C_  B  ->  ( -.  A  =  B  <->  -.  B  C_  A )
)
54pm5.32i 619 . 2  |-  ( ( A  C_  B  /\  -.  A  =  B
)  <->  ( A  C_  B  /\  -.  B  C_  A ) )
61, 5bitri 241 1  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  B  C_  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    /\ wa 359    = wceq 1652    C_ wss 3312    C. wpss 3313
This theorem is referenced by:  pssirr  3439  pssn2lp  3440  ssnpss  3442  nsspssun  3566  npss0  3658  pssdifcom1  3705  pssdifcom2  3706  php3  7285  fincssdom  8195  reclem2pr  8917  islbs3  16219  chpsscon3  22997  chpssati  23858  fundmpss  25382  lpssat  29738  lssat  29741  dihglblem6  32065
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-ne 2600  df-in 3319  df-ss 3326  df-pss 3328
  Copyright terms: Public domain W3C validator