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

Theorem dfpss3 3521
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 3520 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
2 eqss 3449 . . . . 5  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
32baib 901 . . . 4  |-  ( A 
C_  B  ->  ( A  =  B  <->  B  C_  A
) )
43notbid 292 . . 3  |-  ( A 
C_  B  ->  ( -.  A  =  B  <->  -.  B  C_  A )
)
54pm5.32i 635 . 2  |-  ( ( A  C_  B  /\  -.  A  =  B
)  <->  ( A  C_  B  /\  -.  B  C_  A ) )
61, 5bitri 249 1  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  B  C_  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    /\ wa 367    = wceq 1399    C_ wss 3406    C. wpss 3407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391  df-ne 2593  df-in 3413  df-ss 3420  df-pss 3422
This theorem is referenced by:  pssirr  3535  pssn2lp  3536  ssnpss  3538  nsspssun  3673  npss0  3798  pssdifcom1  3846  pssdifcom2  3847  php3  7644  fincssdom  8638  reclem2pr  9359  ressval3d  14721  islbs3  17937  chpsscon3  26563  chpssati  27423  fundmpss  29402  lpssat  35190  lssat  35193  dihglblem6  37519
  Copyright terms: Public domain W3C validator