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

Theorem dfpss2 4088
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 3971 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 2941 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 623 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 275 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395   = wceq 1540  wne 2940  wss 3951  wpss 3952
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 207  df-an 396  df-ne 2941  df-pss 3971
This theorem is referenced by:  dfpss3  4089  sspss  4102  psstr  4107  npss  4113  ssnelpss  4114  pssv  4449  disj4  4459  f1imapss  7286  pssnn  9208  phpeqd  9252  phpeqdOLD  9262  nnsdomo  9270  inf3lem6  9673  ssfin4  10350  fin23lem25  10364  fin23lem38  10389  isf32lem2  10394  pwfseqlem4  10702  genpcl  11048  prlem934  11073  ltaddpr  11074  sltlpss  27945  chnlei  31504  cvbr2  32302  cvnbtwn2  32306  cvnbtwn3  32307  cvnbtwn4  32308  dfon2lem3  35786  dfon2lem5  35788  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  dfon3  35893  lcvbr2  39023  lcvnbtwn2  39028  lcvnbtwn3  39029  rr-phpd  44222
  Copyright terms: Public domain W3C validator