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

Theorem dfpss2 4048
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 3938 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
2 df-ne 3015 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
32anbi2i 625 . 2 ((𝐴𝐵𝐴𝐵) ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
41, 3bitri 278 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wa 399   = wceq 1538  wne 3014  wss 3919  wpss 3920
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 210  df-an 400  df-ne 3015  df-pss 3938
This theorem is referenced by:  dfpss3  4049  sspss  4062  psstr  4067  npss  4073  ssnelpss  4074  pssv  4381  disj4  4391  f1imapss  7016  phpeqd  8703  nnsdomo  8711  pssnn  8733  inf3lem6  9093  ssfin4  9730  fin23lem25  9744  fin23lem38  9769  isf32lem2  9774  pwfseqlem4  10082  genpcl  10428  prlem934  10453  ltaddpr  10454  chnlei  29275  cvbr2  30073  cvnbtwn2  30077  cvnbtwn3  30078  cvnbtwn4  30079  dfon2lem3  33091  dfon2lem5  33093  dfon2lem6  33094  dfon2lem7  33095  dfon2lem8  33096  dfon3  33414  lcvbr2  36267  lcvnbtwn2  36272  lcvnbtwn3  36273  rr-phpd  40841
  Copyright terms: Public domain W3C validator