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 30372). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4054). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3920). Other possible definitions are given by dfpss2 4039 and dfpss3 4040. (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 2925	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4039  psseq1  4041  psseq2  4042  pssss  4049  pssne  4050  nssinpss  4218  pssdif  4320  0pss  4398  difsnpss  4758  ordelpss  6335  fisseneq  9152  ominf  9153  f1finf1o  9162  fofinf1o  9222  inf3lem2  9525  inf3lem4  9527  infeq5  9533  fin23lem31  10237  isf32lem6  10252  ipolt  18441  lssnle  19553  pgpfaclem2  19963  lspsncv0  21053  islbs3  21062  lbsextlem4  21068  lidlnz  21149  filssufilg  23796  alexsubALTlem4  23935  ppiltx  27085  ex-pss  30372  ch0pss  31389  exsslsb  33569  nepss  35701  dfon2  35776  relowlpssretop  37348  finxpreclem3  37377  fin2solem  37596  lshpnelb  38973  lshpcmp  38977  lsatssn0  38991  lcvbr3  39012  lsatcv0  39020  lsat0cv  39022  lcvexchlem1  39023  islshpcv  39042  lkrpssN  39152  lkreqN  39159  osumcllem11N  39955  pexmidlem8N  39966  dochsordN  41363  dochsat  41372  dochshpncl  41373  dochexmidlem8  41456  mapdsord  41644  psspwb  42211  xppss12  42212  omssrncard  43523  trelpss  44438  isomenndlem  46521  lvecpsslmod  48502