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

Theorem dfpss3 3654
Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
dfpss3 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))

Proof of Theorem dfpss3
StepHypRef Expression
1 dfpss2 3653 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
2 eqss 3582 . . . . 5 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
32baib 941 . . . 4 (𝐴𝐵 → (𝐴 = 𝐵𝐵𝐴))
43notbid 306 . . 3 (𝐴𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵𝐴))
54pm5.32i 666 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))
61, 5bitri 262 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wa 382   = wceq 1474  wss 3539  wpss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-ne 2781  df-in 3546  df-ss 3553  df-pss 3555
This theorem is referenced by:  pssirr  3668  pssn2lp  3669  ssnpss  3671  nsspssun  3818  npss0OLD  3966  pssdifcom1  4005  pssdifcom2  4006  php3  8008  fincssdom  9005  reclem2pr  9726  ressval3d  15712  islbs3  18924  chpsscon3  27539  chpssati  28399  fundmpss  30703  lpssat  33101  lssat  33104  dihglblem6  35430  pssnssi  38095  mbfpsssmf  39452
  Copyright terms: Public domain W3C validator