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

Definition df-pss 3729
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 27594). Note that ¬ 𝐴𝐴 (proved in pssirr 3847). Contrast this relationship with the relationship 𝐴𝐵 (as defined in df-ss 3727). Other possible definitions are given by dfpss2 3832 and dfpss3 3833. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
df-pss (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))

Detailed syntax breakdown of Definition df-pss
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wpss 3714 . 2 wff 𝐴𝐵
41, 2wss 3713 . . 3 wff 𝐴𝐵
51, 2wne 2930 . . 3 wff 𝐴𝐵
64, 5wa 383 . 2 wff (𝐴𝐵𝐴𝐵)
73, 6wb 196 1 wff (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  dfpss2  3832  psseq1  3834  psseq2  3835  pssss  3842  pssne  3843  nssinpss  3997  pssdif  4086  0pss  4154  difsnpss  4481  ordelpss  5910  fisseneq  8334  ominf  8335  f1finf1o  8350  fofinf1o  8404  inf3lem2  8697  inf3lem4  8699  infeq5  8705  fin23lem31  9355  isf32lem6  9370  ipolt  17358  lssnle  18285  pgpfaclem2  18679  lspsncv0  19346  islbs3  19355  lbsextlem4  19361  lidlnz  19428  filssufilg  21914  alexsubALTlem4  22053  ppiltx  25100  ex-pss  27594  ch0pss  28611  nepss  31904  dfon2  32000  relowlpssretop  33521  finxpreclem3  33539  fin2solem  33706  lshpnelb  34772  lshpcmp  34776  lsatssn0  34790  lcvbr3  34811  lsatcv0  34819  lsat0cv  34821  lcvexchlem1  34822  islshpcv  34841  lkrpssN  34951  lkreqN  34958  osumcllem11N  35753  pexmidlem8N  35764  dochsordN  37163  dochsat  37172  dochshpncl  37173  dochexmidlem8  37256  mapdsord  37444  trelpss  39159  isomenndlem  41248  lvecpsslmod  42804
  Copyright terms: Public domain W3C validator