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

Theorem dfpss2 4059
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 3951 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 3014 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 622 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 276 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396   = wceq 1528  wne 3013  wss 3933  wpss 3934
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 208  df-an 397  df-ne 3014  df-pss 3951
This theorem is referenced by:  dfpss3  4060  sspss  4073  psstr  4078  npss  4084  ssnelpss  4085  pssv  4394  disj4  4404  f1imapss  7015  phpeqd  8694  nnsdomo  8701  pssnn  8724  inf3lem6  9084  ssfin4  9720  fin23lem25  9734  fin23lem38  9759  isf32lem2  9764  pwfseqlem4  10072  genpcl  10418  prlem934  10443  ltaddpr  10444  chnlei  29189  cvbr2  29987  cvnbtwn2  29991  cvnbtwn3  29992  cvnbtwn4  29993  dfon2lem3  32927  dfon2lem5  32929  dfon2lem6  32930  dfon2lem7  32931  dfon2lem8  32932  dfon3  33250  lcvbr2  36038  lcvnbtwn2  36043  lcvnbtwn3  36044  rr-phpd  40439
  Copyright terms: Public domain W3C validator