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

Theorem dfpss2 3575
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 3477 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
2 df-ne 2651 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
32anbi2i 692 . 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 367    = wceq 1398    =/= wne 2649    C_ wss 3461    C. wpss 3462
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 369  df-ne 2651  df-pss 3477
This theorem is referenced by:  dfpss3  3576  sspss  3589  psstr  3594  npss  3600  pssv  3854  disj4  3863  ssnelpss  3878  f1imapss  6149  nnsdomo  7705  pssnn  7731  inf3lem6  8041  ssfin4  8681  fin23lem25  8695  fin23lem38  8720  isf32lem2  8725  pwfseqlem4  9029  genpcl  9375  prlem934  9400  ltaddpr  9401  isprm2lem  14311  chnlei  26604  cvbr2  27403  cvnbtwn2  27407  cvnbtwn3  27408  cvnbtwn4  27409  dfon2lem3  29460  dfon2lem5  29462  dfon2lem6  29463  dfon2lem7  29464  dfon2lem8  29465  dfon3  29773  lcvbr2  35163  lcvnbtwn2  35168  lcvnbtwn3  35169
  Copyright terms: Public domain W3C validator