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

Theorem dfpss2 3654
 Description: Alternate definition of proper subclass. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
dfpss2 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))

Proof of Theorem dfpss2
StepHypRef Expression
1 df-pss 3556 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 2782 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 726 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 263 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   ∧ wa 383   = wceq 1475   ≠ wne 2780   ⊆ wss 3540   ⊊ wpss 3541 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 196  df-an 385  df-ne 2782  df-pss 3556 This theorem is referenced by:  dfpss3  3655  sspss  3668  psstr  3673  npss  3679  ssnelpss  3680  pssv  3968  disj4  3977  f1imapss  6424  nnsdomo  8040  pssnn  8063  inf3lem6  8413  ssfin4  9015  fin23lem25  9029  fin23lem38  9054  isf32lem2  9059  pwfseqlem4  9363  genpcl  9709  prlem934  9734  ltaddpr  9735  isprm2lem  15232  chnlei  27728  cvbr2  28526  cvnbtwn2  28530  cvnbtwn3  28531  cvnbtwn4  28532  dfon2lem3  30934  dfon2lem5  30936  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  dfon3  31169  lcvbr2  33327  lcvnbtwn2  33332  lcvnbtwn3  33333
 Copyright terms: Public domain W3C validator