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

Theorem dfpss3 4084
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 4083 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
2 eqss 3995 . . . . 5 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
32baib 537 . . . 4 (𝐴𝐵 → (𝐴 = 𝐵𝐵𝐴))
43notbid 318 . . 3 (𝐴𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵𝐴))
54pm5.32i 576 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))
61, 5bitri 275 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397   = wceq 1542  wss 3946  wpss 3947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-in 3953  df-ss 3963  df-pss 3965
This theorem is referenced by:  pssirr  4098  pssn2lp  4099  ssnpss  4101  nsspssun  4255  pssdifcom1  4487  pssdifcom2  4488  php3  9207  php3OLD  9219  fincssdom  10313  reclem2pr  11038  ressval3d  17186  ressval3dOLD  17187  islbs3  20755  sltlpss  27380  chpsscon3  30733  chpssati  31593  fundmpss  34675  lpssat  37820  lssat  37823  dihglblem6  40148  pssnssi  43722  mbfpsssmf  45433
  Copyright terms: Public domain W3C validator