Definition df-pss 3910

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 30495). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4044). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3907). Other possible definitions are given by dfpss2 4029 and dfpss3 4030. (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 3891	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3890	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2933	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4029  psseq1  4031  psseq2  4032  pssss  4039  pssne  4040  nssinpss  4208  pssdif  4310  0pss  4388  difsnpss  4753  ordelpss  6349  fisseneq  9170  ominf  9171  f1finf1o  9180  fofinf1o  9239  inf3lem2  9547  inf3lem4  9549  infeq5  9555  fin23lem31  10262  isf32lem6  10277  ipolt  18498  lssnle  19646  pgpfaclem2  20056  lspsncv0  21141  islbs3  21150  lbsextlem4  21156  lidlnz  21237  filssufilg  23873  alexsubALTlem4  24012  ppiltx  27137  ex-pss  30495  ch0pss  31513  exsslsb  33738  nepss  35897  dfon2  35969  relowlpssretop  37677  finxpreclem3  37706  fin2solem  37924  lshpnelb  39427  lshpcmp  39431  lsatssn0  39445  lcvbr3  39466  lsatcv0  39474  lsat0cv  39476  lcvexchlem1  39477  islshpcv  39496  lkrpssN  39606  lkreqN  39613  osumcllem11N  40409  pexmidlem8N  40420  dochsordN  41817  dochsat  41826  dochshpncl  41827  dochexmidlem8  41910  mapdsord  42098  psspwb  42666  xppss12  42667  omssrncard  43964  trelpss  44878  isomenndlem  46955  lvecpsslmod  48974