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 3953
Description: Define proper subclass (or strict subclass) relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 28135). Note that ¬ 𝐴𝐴 (proved in pssirr 4076). Contrast this relationship with the relationship 𝐴𝐵 (as defined in df-ss 3951). Other possible definitions are given by dfpss2 4061 and dfpss3 4062. (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 3936 . 2 wff 𝐴𝐵
41, 2wss 3935 . . 3 wff 𝐴𝐵
51, 2wne 3016 . . 3 wff 𝐴𝐵
64, 5wa 396 . 2 wff (𝐴𝐵𝐴𝐵)
73, 6wb 207 1 wff (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  dfpss2  4061  psseq1  4063  psseq2  4064  pssss  4071  pssne  4072  nssinpss  4232  pssdif  4325  0pss  4394  difsnpss  4734  ordelpss  6213  fisseneq  8718  ominf  8719  f1finf1o  8734  fofinf1o  8788  inf3lem2  9081  inf3lem4  9083  infeq5  9089  fin23lem31  9754  isf32lem6  9769  ipolt  17759  lssnle  18731  pgpfaclem2  19135  lspsncv0  19849  islbs3  19858  lbsextlem4  19864  lidlnz  19931  filssufilg  22449  alexsubALTlem4  22588  ppiltx  25682  ex-pss  28135  ch0pss  29150  nepss  32846  dfon2  32935  relowlpssretop  34528  finxpreclem3  34557  fin2solem  34760  lshpnelb  36002  lshpcmp  36006  lsatssn0  36020  lcvbr3  36041  lsatcv0  36049  lsat0cv  36051  lcvexchlem1  36052  islshpcv  36071  lkrpssN  36181  lkreqN  36188  osumcllem11N  36984  pexmidlem8N  36995  dochsordN  38392  dochsat  38401  dochshpncl  38402  dochexmidlem8  38485  mapdsord  38673  psspwb  38994  xppss12  38995  trelpss  40667  isomenndlem  42693  lvecpsslmod  44460
  Copyright terms: Public domain W3C validator