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

Theorem dfpss2 3375
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 3279 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
2 df-ne 2552 . . 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 1649    =/= wne 2550    C_ wss 3263    C. wpss 3264
This theorem is referenced by:  dfpss3  3376  sspss  3389  psstr  3394  npss  3400  pssv  3610  disj4  3619  ssnelpss  3634  f1imapss  5951  nnsdomo  7237  pssnn  7263  inf3lem6  7521  ssfin4  8123  fin23lem25  8137  fin23lem38  8162  isf32lem2  8167  pwfseqlem4  8470  genpcl  8818  prlem934  8843  ltaddpr  8844  isprm2lem  13013  chnlei  22835  cvbr2  23634  cvnbtwn2  23638  cvnbtwn3  23639  cvnbtwn4  23640  dfon2lem3  25165  dfon2lem5  25167  dfon2lem6  25168  dfon2lem7  25169  dfon2lem8  25170  dfon3  25456  lcvbr2  29137  lcvnbtwn2  29142  lcvnbtwn3  29143
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 2552  df-pss 3279
  Copyright terms: Public domain W3C validator