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

Theorem dfpss2 4050
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 3934 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 2945 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 624 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 275 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397   = wceq 1542  wne 2944  wss 3915  wpss 3916
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 398  df-ne 2945  df-pss 3934
This theorem is referenced by:  dfpss3  4051  sspss  4064  psstr  4069  npss  4075  ssnelpss  4076  pssv  4411  disj4  4423  f1imapss  7218  pssnn  9119  phpeqd  9166  phpeqdOLD  9176  nnsdomo  9185  pssnnOLD  9216  inf3lem6  9576  ssfin4  10253  fin23lem25  10267  fin23lem38  10292  isf32lem2  10297  pwfseqlem4  10605  genpcl  10951  prlem934  10976  ltaddpr  10977  sltlpss  27258  chnlei  30469  cvbr2  31267  cvnbtwn2  31271  cvnbtwn3  31272  cvnbtwn4  31273  dfon2lem3  34399  dfon2lem5  34401  dfon2lem6  34402  dfon2lem7  34403  dfon2lem8  34404  dfon3  34506  lcvbr2  37513  lcvnbtwn2  37518  lcvnbtwn3  37519  rr-phpd  42557
  Copyright terms: Public domain W3C validator