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

Theorem dfpss2 3653
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 3555 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 2781 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 725 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 262 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wa 382   = wceq 1474  wne 2779  wss 3539  wpss 3540
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 195  df-an 384  df-ne 2781  df-pss 3555
This theorem is referenced by:  dfpss3  3654  sspss  3667  psstr  3672  npss  3678  ssnelpss  3679  pssv  3967  disj4  3976  f1imapss  6401  nnsdomo  8017  pssnn  8040  inf3lem6  8390  ssfin4  8992  fin23lem25  9006  fin23lem38  9031  isf32lem2  9036  pwfseqlem4  9340  genpcl  9686  prlem934  9711  ltaddpr  9712  isprm2lem  15180  chnlei  27521  cvbr2  28319  cvnbtwn2  28323  cvnbtwn3  28324  cvnbtwn4  28325  dfon2lem3  30727  dfon2lem5  30729  dfon2lem6  30730  dfon2lem7  30731  dfon2lem8  30732  dfon3  30962  lcvbr2  33110  lcvnbtwn2  33115  lcvnbtwn3  33116
  Copyright terms: Public domain W3C validator