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

Theorem dfpss2 3914
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 3808 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 2970 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 616 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 267 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wa 386   = wceq 1601  wne 2969  wss 3792  wpss 3793
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 199  df-an 387  df-ne 2970  df-pss 3808
This theorem is referenced by:  dfpss3  3915  sspss  3928  psstr  3933  npss  3939  ssnelpss  3940  pssv  4241  disj4  4251  f1imapss  6797  nnsdomo  8445  pssnn  8468  inf3lem6  8829  ssfin4  9469  fin23lem25  9483  fin23lem38  9508  isf32lem2  9513  pwfseqlem4  9821  genpcl  10167  prlem934  10192  ltaddpr  10193  chnlei  28933  cvbr2  29731  cvnbtwn2  29735  cvnbtwn3  29736  cvnbtwn4  29737  dfon2lem3  32286  dfon2lem5  32288  dfon2lem6  32289  dfon2lem7  32290  dfon2lem8  32291  dfon3  32596  lcvbr2  35185  lcvnbtwn2  35190  lcvnbtwn3  35191
  Copyright terms: Public domain W3C validator