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

Theorem dfpss2 3725
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 3623 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 2824 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 730 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 264 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 383   = wceq 1523  wne 2823  wss 3607  wpss 3608
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 197  df-an 385  df-ne 2824  df-pss 3623
This theorem is referenced by:  dfpss3  3726  sspss  3739  psstr  3744  npss  3750  ssnelpss  3751  pssv  4049  disj4  4058  f1imapss  6563  nnsdomo  8196  pssnn  8219  inf3lem6  8568  ssfin4  9170  fin23lem25  9184  fin23lem38  9209  isf32lem2  9214  pwfseqlem4  9522  genpcl  9868  prlem934  9893  ltaddpr  9894  chnlei  28472  cvbr2  29270  cvnbtwn2  29274  cvnbtwn3  29275  cvnbtwn4  29276  dfon2lem3  31814  dfon2lem5  31816  dfon2lem6  31817  dfon2lem7  31818  dfon2lem8  31819  dfon3  32124  lcvbr2  34627  lcvnbtwn2  34632  lcvnbtwn3  34633
  Copyright terms: Public domain W3C validator