Definition df-pss 3917

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 30408). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4050). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3914). Other possible definitions are given by dfpss2 4035 and dfpss3 4036. (Contributed by NM, 7-Feb-1996.)

Assertion

Ref	Expression
df-pss	⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

Detailed syntax breakdown of Definition df-pss

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wpss 3898	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3897	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2928	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4035  psseq1  4037  psseq2  4038  pssss  4045  pssne  4046  nssinpss  4214  pssdif  4316  0pss  4394  difsnpss  4756  ordelpss  6334  fisseneq  9147  ominf  9148  f1finf1o  9157  fofinf1o  9216  inf3lem2  9519  inf3lem4  9521  infeq5  9527  fin23lem31  10234  isf32lem6  10249  ipolt  18441  lssnle  19586  pgpfaclem2  19996  lspsncv0  21083  islbs3  21092  lbsextlem4  21098  lidlnz  21179  filssufilg  23826  alexsubALTlem4  23965  ppiltx  27114  ex-pss  30408  ch0pss  31425  exsslsb  33609  nepss  35762  dfon2  35834  relowlpssretop  37408  finxpreclem3  37437  fin2solem  37656  lshpnelb  39093  lshpcmp  39097  lsatssn0  39111  lcvbr3  39132  lsatcv0  39140  lsat0cv  39142  lcvexchlem1  39143  islshpcv  39162  lkrpssN  39272  lkreqN  39279  osumcllem11N  40075  pexmidlem8N  40086  dochsordN  41483  dochsat  41492  dochshpncl  41493  dochexmidlem8  41576  mapdsord  41764  psspwb  42331  xppss12  42332  omssrncard  43643  trelpss  44557  isomenndlem  46638  lvecpsslmod  48618