Definition df-pss 3904

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 30518). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4036). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3901). Other possible definitions are given by dfpss2 4021 and dfpss3 4022. (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 3885	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3884	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2936	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 397	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 208	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4021  psseq1  4023  psseq2  4024  pssss  4031  pssne  4032  nssinpss  4197  pssdif  4299  0pss  4377  difsnpss  4742  ordelpss  6341  fisseneq  9167  ominf  9168  f1finf1o  9177  fofinf1o  9236  inf3lem2  9545  inf3lem4  9547  infeq5  9553  fin23lem31  10261  isf32lem6  10276  ipolt  18496  lssnle  19643  pgpfaclem2  20053  lspsncv0  21142  islbs3  21151  lbsextlem4  21157  lidlnz  21238  filssufilg  23897  alexsubALTlem4  24036  ppiltx  27161  ex-pss  30518  ch0pss  31536  exsslsb  33791  nepss  35959  dfon2  36031  relowlpssretop  37739  finxpreclem3  37768  fin2solem  37986  lshpnelb  39489  lshpcmp  39493  lsatssn0  39507  lcvbr3  39528  lsatcv0  39536  lsat0cv  39538  lcvexchlem1  39539  islshpcv  39558  lkrpssN  39668  lkreqN  39675  osumcllem11N  40471  pexmidlem8N  40482  dochsordN  41879  dochsat  41888  dochshpncl  41889  dochexmidlem8  41972  mapdsord  42160  psspwb  42728  xppss12  42729  omssrncard  43997  trelpss  44911  isomenndlem  46985  lvecpsslmod  49010