Definition df-pss 3555

Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 26470). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 3668). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3553). Other possible definitions are given by dfpss2 3653 and dfpss3 3654. (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 3540	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3539	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2779	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 382	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 194	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  3653  psseq1  3655  psseq2  3656  pssss  3663  pssne  3664  nssinpss  3817  pssdif  3898  0pss  3964  difsnpss  4278  ordelpss  5653  fisseneq  8033  ominf  8034  f1finf1o  8049  fofinf1o  8103  inf3lem2  8386  inf3lem4  8388  infeq5  8394  fin23lem31  9025  isf32lem6  9040  ipolt  16930  lssnle  17858  pgpfaclem2  18252  lspsncv0  18915  islbs3  18924  lbsextlem4  18930  lidlnz  18997  filssufilg  21472  alexsubALTlem4  21611  ppiltx  24647  ex-pss  26470  ch0pss  27481  nepss  30647  dfon2  30734  relowlpssretop  32171  finxpreclem3  32189  fin2solem  32348  lshpnelb  33072  lshpcmp  33076  lsatssn0  33090  lcvbr3  33111  lsatcv0  33119  lsat0cv  33121  lcvexchlem1  33122  islshpcv  33141  lkrpssN  33251  lkreqN  33258  osumcllem11N  34053  pexmidlem8N  34064  dochsordN  35464  dochsat  35473  dochshpncl  35474  dochexmidlem8  35557  mapdsord  35745  trelpss  37463  isomenndlem  39203  lvecpsslmod  42071