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

Theorem dfpss2 3261
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 3168 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
2 df-ne 2448 . . 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 1623    =/= wne 2446    C_ wss 3152    C. wpss 3153
This theorem is referenced by:  dfpss3  3262  sspss  3275  psstr  3280  npss  3286  pssv  3494  disj4  3503  ssnelpss  3517  f1imapss  5790  nnsdomo  7055  pssnn  7081  inf3lem6  7334  ssfin4  7936  fin23lem25  7950  fin23lem38  7975  isf32lem2  7980  pwfseqlem4  8284  genpcl  8632  prlem934  8657  ltaddpr  8658  isprm2lem  12765  chnlei  22064  cvbr2  22863  cvnbtwn2  22867  cvnbtwn3  22868  cvnbtwn4  22869  dfon2lem3  24141  dfon2lem5  24143  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  dfon3  24432  lcvbr2  29212  lcvnbtwn2  29217  lcvnbtwn3  29218
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 2448  df-pss 3168
  Copyright terms: Public domain W3C validator