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

Theorem dfpss2 3539
Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
dfpss2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )

Proof of Theorem dfpss2
StepHypRef Expression
1 df-pss 3442 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
2 df-ne 2646 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
32anbi2i 694 . 2  |-  ( ( A  C_  B  /\  A  =/=  B )  <->  ( A  C_  B  /\  -.  A  =  B ) )
41, 3bitri 249 1  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    /\ wa 369    = wceq 1370    =/= wne 2644    C_ wss 3426    C. wpss 3427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-ne 2646  df-pss 3442
This theorem is referenced by:  dfpss3  3540  sspss  3553  psstr  3558  npss  3564  pssv  3816  disj4  3825  ssnelpss  3840  f1imapss  6078  nnsdomo  7606  pssnn  7632  inf3lem6  7940  ssfin4  8580  fin23lem25  8594  fin23lem38  8619  isf32lem2  8624  pwfseqlem4  8930  genpcl  9278  prlem934  9303  ltaddpr  9304  isprm2lem  13872  chnlei  25023  cvbr2  25822  cvnbtwn2  25826  cvnbtwn3  25827  cvnbtwn4  25828  dfon2lem3  27732  dfon2lem5  27734  dfon2lem6  27735  dfon2lem7  27736  dfon2lem8  27737  dfon3  28057  lcvbr2  32973  lcvnbtwn2  32978  lcvnbtwn3  32979
  Copyright terms: Public domain W3C validator