Definition df-pss 3924

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 30790). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4056). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3921). Other possible definitions are given by dfpss2 4041 and dfpss3 4042. (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 3905	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3904	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2957	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 400	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is used by:  dfpss2  4041  psseq1  4043  psseq2  4044  pssss  4051  pssne  4052  nssinpss  4219  pssdif  4323  0pss  4366  difsnpss  4774  ordelpss  6388  fisseneq  9221  ominf  9222  f1finf1o  9231  fofinf1o  9287  inf3lem2  9596  inf3lem4  9598  infeq5  9604  fin23lem31  10333  isf32lem6  10348  ipolt  18597  lssnle  19750  pgpfaclem2  20160  lspsncv0  21281  islbs3  21290  lbsextlem4  21296  lidlnz  21387  filssufilg  24079  alexsubALTlem4  24218  ppiltx  27352  ex-pss  30790  ch0pss  31808  exsslsb  33996  nepss  36218  dfon2  36290  relowlpssretop  38038  finxpreclem3  38067  fin2solem  38285  lshpnelb  39786  lshpcmp  39790  lsatssn0  39804  lcvbr3  39825  lsatcv0  39833  lsat0cv  39835  lcvexchlem1  39836  islshpcv  39855  lkrpssN  39965  lkreqN  39972  osumcllem11N  40768  pexmidlem8N  40779  dochsordN  42176  dochsat  42185  dochshpncl  42186  dochexmidlem8  42269  mapdsord  42457  psspwb  43027  xppss12  43028  omssrncard  44294  trelpss  45191  isomenndlem  47272  lvecpsslmod  49315