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

Theorem dfpss3 3376
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 3375 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
2 eqss 3306 . . . . 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 1649    C_ wss 3263    C. wpss 3264
This theorem is referenced by:  pssirr  3390  pssn2lp  3391  ssnpss  3393  nsspssun  3517  npss0  3609  pssdifcom1  3656  pssdifcom2  3657  php3  7229  fincssdom  8136  reclem2pr  8858  islbs3  16154  chpsscon3  22853  chpssati  23714  fundmpss  25146  lpssat  29128  lssat  29131  dihglblem6  31455
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 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-ne 2552  df-in 3270  df-ss 3277  df-pss 3279
  Copyright terms: Public domain W3C validator