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

Theorem dfpss2 3274
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 3181 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
2 df-ne 2461 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
32anbi2i 675 . 2  |-  ( ( A  C_  B  /\  A  =/=  B )  <->  ( A  C_  B  /\  -.  A  =  B ) )
41, 3bitri 240 1  |-  ( A 
C.  B  <->  ( A  C_  B  /\  -.  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    /\ wa 358    = wceq 1632    =/= wne 2459    C_ wss 3165    C. wpss 3166
This theorem is referenced by:  dfpss3  3275  sspss  3288  psstr  3293  npss  3299  pssv  3507  disj4  3516  ssnelpss  3530  f1imapss  5806  nnsdomo  7071  pssnn  7097  inf3lem6  7350  ssfin4  7952  fin23lem25  7966  fin23lem38  7991  isf32lem2  7996  pwfseqlem4  8300  genpcl  8648  prlem934  8673  ltaddpr  8674  isprm2lem  12781  chnlei  22080  cvbr2  22879  cvnbtwn2  22883  cvnbtwn3  22884  cvnbtwn4  22885  dfon2lem3  24212  dfon2lem5  24214  dfon2lem6  24215  dfon2lem7  24216  dfon2lem8  24217  dfon3  24503  lcvbr2  29834  lcvnbtwn2  29839  lcvnbtwn3  29840
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 177  df-an 360  df-ne 2461  df-pss 3181
  Copyright terms: Public domain W3C validator