Definition df-pss 3919

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

This definition is referenced by:  dfpss2  4038  psseq1  4040  psseq2  4041  pssss  4048  pssne  4049  nssinpss  4217  pssdif  4319  0pss  4397  difsnpss  4761  ordelpss  6343  fisseneq  9161  ominf  9162  f1finf1o  9171  fofinf1o  9230  inf3lem2  9536  inf3lem4  9538  infeq5  9544  fin23lem31  10251  isf32lem6  10266  ipolt  18456  lssnle  19601  pgpfaclem2  20011  lspsncv0  21099  islbs3  21108  lbsextlem4  21114  lidlnz  21195  filssufilg  23853  alexsubALTlem4  23992  ppiltx  27141  ex-pss  30452  ch0pss  31469  exsslsb  33702  nepss  35861  dfon2  35933  relowlpssretop  37508  finxpreclem3  37537  fin2solem  37746  lshpnelb  39183  lshpcmp  39187  lsatssn0  39201  lcvbr3  39222  lsatcv0  39230  lsat0cv  39232  lcvexchlem1  39233  islshpcv  39252  lkrpssN  39362  lkreqN  39369  osumcllem11N  40165  pexmidlem8N  40176  dochsordN  41573  dochsat  41582  dochshpncl  41583  dochexmidlem8  41666  mapdsord  41854  psspwb  42426  xppss12  42427  omssrncard  43723  trelpss  44637  isomenndlem  46716  lvecpsslmod  48695