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 30745). 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 2956	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 400	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4041  psseq1  4043  psseq2  4044  pssss  4051  pssne  4052  nssinpss  4219  pssdif  4323  0pss  4366  difsnpss  4774  ordelpss  6388  fisseneq  9222  ominf  9223  f1finf1o  9232  fofinf1o  9288  inf3lem2  9597  inf3lem4  9599  infeq5  9605  fin23lem31  10326  isf32lem6  10341  ipolt  18590  lssnle  19743  pgpfaclem2  20153  lspsncv0  21249  islbs3  21258  lbsextlem4  21264  lidlnz  21355  filssufilg  24047  alexsubALTlem4  24186  ppiltx  27317  ex-pss  30745  ch0pss  31763  exsslsb  33953  nepss  36164  dfon2  36236  relowlpssretop  37954  finxpreclem3  37983  fin2solem  38201  lshpnelb  39704  lshpcmp  39708  lsatssn0  39722  lcvbr3  39743  lsatcv0  39751  lsat0cv  39753  lcvexchlem1  39754  islshpcv  39773  lkrpssN  39883  lkreqN  39890  osumcllem11N  40686  pexmidlem8N  40697  dochsordN  42094  dochsat  42103  dochshpncl  42104  dochexmidlem8  42187  mapdsord  42375  psspwb  42945  xppss12  42946  omssrncard  44214  trelpss  45111  isomenndlem  47192  lvecpsslmod  49232