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

Theorem dfpss3 4087
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 4086 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
2 eqss 3998 . . . . 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 3949  wpss 3950
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 3956  df-ss 3966  df-pss 3968
This theorem is referenced by:  pssirr  4101  pssn2lp  4102  ssnpss  4104  nsspssun  4258  pssdifcom1  4490  pssdifcom2  4491  php3  9212  php3OLD  9224  fincssdom  10318  reclem2pr  11043  ressval3d  17191  ressval3dOLD  17192  islbs3  20768  sltlpss  27402  chpsscon3  30787  chpssati  31647  fundmpss  34769  lpssat  37931  lssat  37934  dihglblem6  40259  pssnssi  43838  mbfpsssmf  45547
  Copyright terms: Public domain W3C validator