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