Definition df-pss 3918

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 30962). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4050). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3915). Other possible definitions are given by dfpss2 4035 and dfpss3 4036. (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 3899	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3898	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2955	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 401	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is used by:  dfpss2  4035  psseq1  4037  psseq2  4038  pssss  4045  pssne  4046  nssinpss  4212  pssdif  4316  0pss  4359  difsnpss  4769  ordelpss  6379  fisseneq  9232  ominf  9233  f1finf1o  9242  fofinf1o  9299  inf3lem2  9608  inf3lem4  9610  infeq5  9616  fin23lem31  10392  isf32lem6  10407  ipolt  18670  lssnle  19849  pgpfaclem2  20259  lspsncv0  21385  islbs3  21394  lbsextlem4  21400  lidlnz  21491  filssufilg  24191  alexsubALTlem4  24330  ppiltx  27467  ex-pss  30962  ch0pss  31980  exsslsb  34162  nepss  36404  dfon2  36476  relowlpssretop  38207  finxpreclem3  38236  fin2solem  38449  lshpnelb  39961  lshpcmp  39965  lsatssn0  39979  lcvbr3  40000  lsatcv0  40008  lsat0cv  40010  lcvexchlem1  40011  islshpcv  40030  lkrpssN  40140  lkreqN  40147  osumcllem11N  40943  pexmidlem8N  40954  dochsordN  42351  dochsat  42360  dochshpncl  42361  dochexmidlem8  42444  mapdsord  42632  psspwb  43202  xppss12  43203  omssrncard  44484  trelpss  45381  isomenndlem  47462  lvecpsslmod  49541