Definition df-pss 3877

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 28312). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4006). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3875). Other possible definitions are given by dfpss2 3991 and dfpss3 3992. (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 3859	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3858	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2951	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 399	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  3991  psseq1  3993  psseq2  3994  pssss  4001  pssne  4002  nssinpss  4161  pssdif  4265  0pss  4341  difsnpss  4697  ordelpss  6197  fisseneq  8767  ominf  8768  f1finf1o  8782  fofinf1o  8832  inf3lem2  9125  inf3lem4  9127  infeq5  9133  fin23lem31  9803  isf32lem6  9818  ipolt  17835  lssnle  18867  pgpfaclem2  19272  lspsncv0  19986  islbs3  19995  lbsextlem4  20001  lidlnz  20069  filssufilg  22611  alexsubALTlem4  22750  ppiltx  25861  ex-pss  28312  ch0pss  29327  nepss  33180  dfon2  33284  relowlpssretop  35061  finxpreclem3  35090  fin2solem  35323  lshpnelb  36560  lshpcmp  36564  lsatssn0  36578  lcvbr3  36599  lsatcv0  36607  lsat0cv  36609  lcvexchlem1  36610  islshpcv  36629  lkrpssN  36739  lkreqN  36746  osumcllem11N  37542  pexmidlem8N  37553  dochsordN  38950  dochsat  38959  dochshpncl  38960  dochexmidlem8  39043  mapdsord  39231  psspwb  39708  xppss12  39709  trelpss  41532  isomenndlem  43535  lvecpsslmod  45281