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 3958
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 28121). Note that ¬ 𝐴𝐴 (proved in pssirr 4081). Contrast this relationship with the relationship 𝐴𝐵 (as defined in df-ss 3956). Other possible definitions are given by dfpss2 4066 and dfpss3 4067. (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 3941 . 2 wff 𝐴𝐵
41, 2wss 3940 . . 3 wff 𝐴𝐵
51, 2wne 3021 . . 3 wff 𝐴𝐵
64, 5wa 396 . 2 wff (𝐴𝐵𝐴𝐵)
73, 6wb 207 1 wff (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  dfpss2  4066  psseq1  4068  psseq2  4069  pssss  4076  pssne  4077  nssinpss  4237  pssdif  4330  0pss  4399  difsnpss  4739  ordelpss  6217  fisseneq  8718  ominf  8719  f1finf1o  8734  fofinf1o  8788  inf3lem2  9081  inf3lem4  9083  infeq5  9089  fin23lem31  9754  isf32lem6  9769  ipolt  17759  lssnle  18720  pgpfaclem2  19124  lspsncv0  19838  islbs3  19847  lbsextlem4  19853  lidlnz  19920  filssufilg  22435  alexsubALTlem4  22574  ppiltx  25668  ex-pss  28121  ch0pss  29136  nepss  32832  dfon2  32921  relowlpssretop  34514  finxpreclem3  34543  fin2solem  34745  lshpnelb  35987  lshpcmp  35991  lsatssn0  36005  lcvbr3  36026  lsatcv0  36034  lsat0cv  36036  lcvexchlem1  36037  islshpcv  36056  lkrpssN  36166  lkreqN  36173  osumcllem11N  36969  pexmidlem8N  36980  dochsordN  38377  dochsat  38386  dochshpncl  38387  dochexmidlem8  38470  mapdsord  38658  psspwb  38979  xppss12  38980  trelpss  40652  isomenndlem  42678  lvecpsslmod  44394
  Copyright terms: Public domain W3C validator