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

Theorem dfpss2 3424
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 3328 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
2 df-ne 2600 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
32anbi2i 676 . 2  |-  ( ( A  C_  B  /\  A  =/=  B )  <->  ( A  C_  B  /\  -.  A  =  B ) )
41, 3bitri 241 1  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    /\ wa 359    = wceq 1652    =/= wne 2598    C_ wss 3312    C. wpss 3313
This theorem is referenced by:  dfpss3  3425  sspss  3438  psstr  3443  npss  3449  pssv  3659  disj4  3668  ssnelpss  3683  f1imapss  6004  nnsdomo  7293  pssnn  7319  inf3lem6  7580  ssfin4  8182  fin23lem25  8196  fin23lem38  8221  isf32lem2  8226  pwfseqlem4  8529  genpcl  8877  prlem934  8902  ltaddpr  8903  isprm2lem  13078  chnlei  22979  cvbr2  23778  cvnbtwn2  23782  cvnbtwn3  23783  cvnbtwn4  23784  dfon2lem3  25404  dfon2lem5  25406  dfon2lem6  25407  dfon2lem7  25408  dfon2lem8  25409  dfon3  25729  lcvbr2  29757  lcvnbtwn2  29762  lcvnbtwn3  29763
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-ne 2600  df-pss 3328
  Copyright terms: Public domain W3C validator