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

Theorem dfpss2 3834
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 3731 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 2933 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 732 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 264 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 383   = wceq 1632  wne 2932  wss 3715  wpss 3716
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 197  df-an 385  df-ne 2933  df-pss 3731
This theorem is referenced by:  dfpss3  3835  sspss  3848  psstr  3853  npss  3859  ssnelpss  3860  pssv  4159  disj4  4169  f1imapss  6687  nnsdomo  8322  pssnn  8345  inf3lem6  8705  ssfin4  9344  fin23lem25  9358  fin23lem38  9383  isf32lem2  9388  pwfseqlem4  9696  genpcl  10042  prlem934  10067  ltaddpr  10068  chnlei  28674  cvbr2  29472  cvnbtwn2  29476  cvnbtwn3  29477  cvnbtwn4  29478  dfon2lem3  32016  dfon2lem5  32018  dfon2lem6  32019  dfon2lem7  32020  dfon2lem8  32021  dfon3  32326  lcvbr2  34830  lcvnbtwn2  34835  lcvnbtwn3  34836
  Copyright terms: Public domain W3C validator