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

Theorem dfpss3 4099
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 4098 . 2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
2 eqss 4011 . . . . 5 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
32baib 535 . . . 4 (𝐴𝐵 → (𝐴 = 𝐵𝐵𝐴))
43notbid 318 . . 3 (𝐴𝐵 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐵𝐴))
54pm5.32i 574 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 = 𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))
61, 5bitri 275 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395   = wceq 1537  wss 3963  wpss 3964
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ne 2939  df-ss 3980  df-pss 3983
This theorem is referenced by:  pssirr  4113  pssn2lp  4114  ssnpss  4116  nsspssun  4274  pssdifcom1  4496  pssdifcom2  4497  php3  9247  php3OLD  9259  fincssdom  10361  reclem2pr  11086  ressval3d  17292  ressval3dOLD  17293  islbs3  21175  sltlpss  27960  chpsscon3  31532  chpssati  32392  fundmpss  35748  lpssat  38995  lssat  38998  dihglblem6  41323  pssnssi  45041  mbfpsssmf  46739
  Copyright terms: Public domain W3C validator