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

Theorem dfpss3 3551
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 3550 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
2 eqss 3480 . . . . 5  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
32baib 896 . . . 4  |-  ( A 
C_  B  ->  ( A  =  B  <->  B  C_  A
) )
43notbid 294 . . 3  |-  ( A 
C_  B  ->  ( -.  A  =  B  <->  -.  B  C_  A )
)
54pm5.32i 637 . 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 369    = wceq 1370    C_ wss 3437    C. wpss 3438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ne 2650  df-in 3444  df-ss 3451  df-pss 3453
This theorem is referenced by:  pssirr  3565  pssn2lp  3566  ssnpss  3568  nsspssun  3692  npss0  3826  pssdifcom1  3873  pssdifcom2  3874  php3  7608  fincssdom  8604  reclem2pr  9329  islbs3  17360  chpsscon3  25059  chpssati  25920  fundmpss  27722  lpssat  32997  lssat  33000  dihglblem6  35324
  Copyright terms: Public domain W3C validator