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

Theorem dfpss2 4083
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 3966 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 2938 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 622 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 275 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 395   = wceq 1534  wne 2937  wss 3947  wpss 3948
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 206  df-an 396  df-ne 2938  df-pss 3966
This theorem is referenced by:  dfpss3  4084  sspss  4097  psstr  4102  npss  4108  ssnelpss  4109  pssv  4447  disj4  4459  f1imapss  7276  pssnn  9192  phpeqd  9239  phpeqdOLD  9249  nnsdomo  9258  pssnnOLD  9289  inf3lem6  9656  ssfin4  10333  fin23lem25  10347  fin23lem38  10372  isf32lem2  10377  pwfseqlem4  10685  genpcl  11031  prlem934  11056  ltaddpr  11057  sltlpss  27832  chnlei  31294  cvbr2  32092  cvnbtwn2  32096  cvnbtwn3  32097  cvnbtwn4  32098  dfon2lem3  35381  dfon2lem5  35383  dfon2lem6  35384  dfon2lem7  35385  dfon2lem8  35386  dfon3  35488  lcvbr2  38494  lcvnbtwn2  38499  lcvnbtwn3  38500  rr-phpd  43640
  Copyright terms: Public domain W3C validator