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 3555
Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 26470). Note that ¬ 𝐴𝐴 (proved in pssirr 3668). Contrast this relationship with the relationship 𝐴𝐵 (as defined in df-ss 3553). Other possible definitions are given by dfpss2 3653 and dfpss3 3654. (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 3540 . 2 wff 𝐴𝐵
41, 2wss 3539 . . 3 wff 𝐴𝐵
51, 2wne 2779 . . 3 wff 𝐴𝐵
64, 5wa 382 . 2 wff (𝐴𝐵𝐴𝐵)
73, 6wb 194 1 wff (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  dfpss2  3653  psseq1  3655  psseq2  3656  pssss  3663  pssne  3664  nssinpss  3817  pssdif  3898  0pss  3964  difsnpss  4278  ordelpss  5653  fisseneq  8033  ominf  8034  f1finf1o  8049  fofinf1o  8103  inf3lem2  8386  inf3lem4  8388  infeq5  8394  fin23lem31  9025  isf32lem6  9040  ipolt  16930  lssnle  17858  pgpfaclem2  18252  lspsncv0  18915  islbs3  18924  lbsextlem4  18930  lidlnz  18997  filssufilg  21472  alexsubALTlem4  21611  ppiltx  24647  ex-pss  26470  ch0pss  27481  nepss  30647  dfon2  30734  relowlpssretop  32171  finxpreclem3  32189  fin2solem  32348  lshpnelb  33072  lshpcmp  33076  lsatssn0  33090  lcvbr3  33111  lsatcv0  33119  lsat0cv  33121  lcvexchlem1  33122  islshpcv  33141  lkrpssN  33251  lkreqN  33258  osumcllem11N  34053  pexmidlem8N  34064  dochsordN  35464  dochsat  35473  dochshpncl  35474  dochexmidlem8  35557  mapdsord  35745  trelpss  37463  isomenndlem  39203  lvecpsslmod  42071
  Copyright terms: Public domain W3C validator