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

Theorem dfpss2 3588
Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
dfpss2

Proof of Theorem dfpss2
StepHypRef Expression
1 df-pss 3491 . 2
2 df-ne 2654 . . 3
32anbi2i 694 . 2
41, 3bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  /\wa 369  =wceq 1395  =/=wne 2652  C_wss 3475  C.wpss 3476
This theorem is referenced by:  dfpss3  3589  sspss  3602  psstr  3607  npss  3613  pssv  3866  disj4  3875  ssnelpss  3890  f1imapss  6174  nnsdomo  7732  pssnn  7758  inf3lem6  8071  ssfin4  8711  fin23lem25  8725  fin23lem38  8750  isf32lem2  8755  pwfseqlem4  9061  genpcl  9407  prlem934  9432  ltaddpr  9433  isprm2lem  14224  chnlei  26403  cvbr2  27202  cvnbtwn2  27206  cvnbtwn3  27207  cvnbtwn4  27208  dfon2lem3  29217  dfon2lem5  29219  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon3  29542  lcvbr2  34747  lcvnbtwn2  34752  lcvnbtwn3  34753
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 371  df-ne 2654  df-pss 3491
  Copyright terms: Public domain W3C validator