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 3576
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 27173). Note that ¬ 𝐴𝐴 (proved in pssirr 3691). Contrast this relationship with the relationship 𝐴𝐵 (as defined in df-ss 3574). Other possible definitions are given by dfpss2 3676 and dfpss3 3677. (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 3561 . 2 wff 𝐴𝐵
41, 2wss 3560 . . 3 wff 𝐴𝐵
51, 2wne 2790 . . 3 wff 𝐴𝐵
64, 5wa 384 . 2 wff (𝐴𝐵𝐴𝐵)
73, 6wb 196 1 wff (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  dfpss2  3676  psseq1  3678  psseq2  3679  pssss  3686  pssne  3687  nssinpss  3840  pssdif  3925  0pss  3991  difsnpss  4314  ordelpss  5720  fisseneq  8131  ominf  8132  f1finf1o  8147  fofinf1o  8201  inf3lem2  8486  inf3lem4  8488  infeq5  8494  fin23lem31  9125  isf32lem6  9140  ipolt  17099  lssnle  18027  pgpfaclem2  18421  lspsncv0  19086  islbs3  19095  lbsextlem4  19101  lidlnz  19168  filssufilg  21655  alexsubALTlem4  21794  ppiltx  24837  ex-pss  27173  ch0pss  28192  nepss  31361  dfon2  31451  relowlpssretop  32883  finxpreclem3  32901  fin2solem  33066  lshpnelb  33790  lshpcmp  33794  lsatssn0  33808  lcvbr3  33829  lsatcv0  33837  lsat0cv  33839  lcvexchlem1  33840  islshpcv  33859  lkrpssN  33969  lkreqN  33976  osumcllem11N  34771  pexmidlem8N  34782  dochsordN  36182  dochsat  36191  dochshpncl  36192  dochexmidlem8  36275  mapdsord  36463  trelpss  38180  isomenndlem  40081  lvecpsslmod  41614
  Copyright terms: Public domain W3C validator