Definition df-pss 3920

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 30398). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4051). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3917). Other possible definitions are given by dfpss2 4036 and dfpss3 4037. (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 3901	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3900	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2926	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4036  psseq1  4038  psseq2  4039  pssss  4046  pssne  4047  nssinpss  4215  pssdif  4317  0pss  4395  difsnpss  4757  ordelpss  6330  fisseneq  9142  ominf  9143  f1finf1o  9152  fofinf1o  9211  inf3lem2  9514  inf3lem4  9516  infeq5  9522  fin23lem31  10226  isf32lem6  10241  ipolt  18433  lssnle  19579  pgpfaclem2  19989  lspsncv0  21076  islbs3  21085  lbsextlem4  21091  lidlnz  21172  filssufilg  23819  alexsubALTlem4  23958  ppiltx  27107  ex-pss  30398  ch0pss  31415  exsslsb  33599  nepss  35730  dfon2  35805  relowlpssretop  37377  finxpreclem3  37406  fin2solem  37625  lshpnelb  39002  lshpcmp  39006  lsatssn0  39020  lcvbr3  39041  lsatcv0  39049  lsat0cv  39051  lcvexchlem1  39052  islshpcv  39071  lkrpssN  39181  lkreqN  39188  osumcllem11N  39984  pexmidlem8N  39995  dochsordN  41392  dochsat  41401  dochshpncl  41402  dochexmidlem8  41485  mapdsord  41673  psspwb  42240  xppss12  42241  omssrncard  43552  trelpss  44466  isomenndlem  46547  lvecpsslmod  48518