Definition df-pss 3954

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 28207). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4077). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3952). Other possible definitions are given by dfpss2 4062 and dfpss3 4063. (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 3937	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3936	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 3016	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 398	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 208	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4062  psseq1  4064  psseq2  4065  pssss  4072  pssne  4073  nssinpss  4233  pssdif  4326  0pss  4396  difsnpss  4740  ordelpss  6219  fisseneq  8729  ominf  8730  f1finf1o  8745  fofinf1o  8799  inf3lem2  9092  inf3lem4  9094  infeq5  9100  fin23lem31  9765  isf32lem6  9780  ipolt  17769  lssnle  18800  pgpfaclem2  19204  lspsncv0  19918  islbs3  19927  lbsextlem4  19933  lidlnz  20001  filssufilg  22519  alexsubALTlem4  22658  ppiltx  25754  ex-pss  28207  ch0pss  29222  nepss  32948  dfon2  33037  relowlpssretop  34648  finxpreclem3  34677  fin2solem  34893  lshpnelb  36135  lshpcmp  36139  lsatssn0  36153  lcvbr3  36174  lsatcv0  36182  lsat0cv  36184  lcvexchlem1  36185  islshpcv  36204  lkrpssN  36314  lkreqN  36321  osumcllem11N  37117  pexmidlem8N  37128  dochsordN  38525  dochsat  38534  dochshpncl  38535  dochexmidlem8  38618  mapdsord  38806  psspwb  39134  xppss12  39135  trelpss  40807  isomenndlem  42832  lvecpsslmod  44582