Definition df-pss 3900

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 28213). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4028). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3898). Other possible definitions are given by dfpss2 4013 and dfpss3 4014. (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 3882	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3881	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2987	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 399	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4013  psseq1  4015  psseq2  4016  pssss  4023  pssne  4024  nssinpss  4183  pssdif  4280  0pss  4352  difsnpss  4700  ordelpss  6187  fisseneq  8713  ominf  8714  f1finf1o  8729  fofinf1o  8783  inf3lem2  9076  inf3lem4  9078  infeq5  9084  fin23lem31  9754  isf32lem6  9769  ipolt  17761  lssnle  18792  pgpfaclem2  19197  lspsncv0  19911  islbs3  19920  lbsextlem4  19926  lidlnz  19994  filssufilg  22516  alexsubALTlem4  22655  ppiltx  25762  ex-pss  28213  ch0pss  29228  nepss  33061  dfon2  33150  relowlpssretop  34781  finxpreclem3  34810  fin2solem  35043  lshpnelb  36280  lshpcmp  36284  lsatssn0  36298  lcvbr3  36319  lsatcv0  36327  lsat0cv  36329  lcvexchlem1  36330  islshpcv  36349  lkrpssN  36459  lkreqN  36466  osumcllem11N  37262  pexmidlem8N  37273  dochsordN  38670  dochsat  38679  dochshpncl  38680  dochexmidlem8  38763  mapdsord  38951  psspwb  39408  xppss12  39409  trelpss  41159  isomenndlem  43169  lvecpsslmod  44916