Definition df-pss 4017

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 31056). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4033). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3901). Other possible definitions are given by dfpss2 4018 and dfpss3 4019. (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 4016	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3900	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2959	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 401	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is used by:  dfpss2  4018  psseq1  4020  psseq2  4021  pssss  4028  pssne  4029  nssinpss  4215  pssdif  4320  0pss  4363  difsnpss  4770  ordelpss  6405  fisseneq  9279  ominf  9280  f1finf1o  9289  fofinf1o  9346  inf3lem2  9654  inf3lem4  9656  infeq5  9662  fin23lem31  10445  isf32lem6  10460  ipolt  18735  lssnle  19915  pgpfaclem2  20325  lspsncv0  21451  islbs3  21460  lbsextlem4  21466  lidlnz  21557  filssufilg  24257  alexsubALTlem4  24396  ppiltx  27531  ex-pss  31056  ch0pss  32074  exsslsb  34296  elpssex  36634  nepss  36660  dfon2  36731  relowlpssretop  38478  finxpreclem3  38507  fin2solem  38720  lshpnelb  40232  lshpcmp  40236  lsatssn0  40250  lcvbr3  40271  lsatcv0  40279  lsat0cv  40281  lcvexchlem1  40282  islshpcv  40301  lkrpssN  40411  lkreqN  40418  osumcllem11N  41214  pexmidlem8N  41225  dochsordN  42622  dochsat  42631  dochshpncl  42632  dochexmidlem8  42715  mapdsord  42903  psspwb  43473  xppss12  43474  omssrncard  44731  trelpss  45626  isomenndlem  47743  lvecpsslmod  49822