Definition df-pss 3923

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 30521). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4057). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3920). Other possible definitions are given by dfpss2 4042 and dfpss3 4043. (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 3904	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3903	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2933	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4042  psseq1  4044  psseq2  4045  pssss  4052  pssne  4053  nssinpss  4221  pssdif  4323  0pss  4401  difsnpss  4765  ordelpss  6355  fisseneq  9177  ominf  9178  f1finf1o  9187  fofinf1o  9246  inf3lem2  9552  inf3lem4  9554  infeq5  9560  fin23lem31  10267  isf32lem6  10282  ipolt  18472  lssnle  19620  pgpfaclem2  20030  lspsncv0  21118  islbs3  21127  lbsextlem4  21133  lidlnz  21214  filssufilg  23872  alexsubALTlem4  24011  ppiltx  27160  ex-pss  30521  ch0pss  31539  exsslsb  33780  nepss  35940  dfon2  36012  relowlpssretop  37646  finxpreclem3  37675  fin2solem  37886  lshpnelb  39389  lshpcmp  39393  lsatssn0  39407  lcvbr3  39428  lsatcv0  39436  lsat0cv  39438  lcvexchlem1  39439  islshpcv  39458  lkrpssN  39568  lkreqN  39575  osumcllem11N  40371  pexmidlem8N  40382  dochsordN  41779  dochsat  41788  dochshpncl  41789  dochexmidlem8  41872  mapdsord  42060  psspwb  42629  xppss12  42630  omssrncard  43925  trelpss  44839  isomenndlem  46917  lvecpsslmod  48896