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

Theorem dfpss3 3856
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 3855 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
2 eqss 3778 . . . . 5 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
32baib 531 . . . 4 (𝐴𝐵 → (𝐴 = 𝐵𝐵𝐴))
43notbid 309 . . 3 (𝐴𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵𝐴))
54pm5.32i 570 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))
61, 5bitri 266 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wa 384   = wceq 1652  wss 3734  wpss 3735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-ne 2938  df-in 3741  df-ss 3748  df-pss 3750
This theorem is referenced by:  pssirr  3870  pssn2lp  3871  ssnpss  3873  nsspssun  4024  pssdifcom1  4216  pssdifcom2  4217  php3  8355  fincssdom  9400  reclem2pr  10125  ressval3d  16212  ressval3dOLD  16213  islbs3  19432  chpsscon3  28821  chpssati  29681  fundmpss  32112  lpssat  34972  lssat  34975  dihglblem6  37299  pssnssi  39936  mbfpsssmf  41634
  Copyright terms: Public domain W3C validator