Definition df-pss 3922

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 30916). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4054). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3919). Other possible definitions are given by dfpss2 4039 and dfpss3 4040. (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 3903	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3902	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2957	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 401	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is used by:  dfpss2  4039  psseq1  4041  psseq2  4042  pssss  4049  pssne  4050  nssinpss  4216  pssdif  4320  0pss  4363  difsnpss  4773  ordelpss  6389  fisseneq  9237  ominf  9238  f1finf1o  9247  fofinf1o  9303  inf3lem2  9612  inf3lem4  9614  infeq5  9620  fin23lem31  10349  isf32lem6  10364  ipolt  18629  lssnle  19807  pgpfaclem2  20217  lspsncv0  21339  islbs3  21348  lbsextlem4  21354  lidlnz  21445  filssufilg  24143  alexsubALTlem4  24282  ppiltx  27421  ex-pss  30916  ch0pss  31934  exsslsb  34115  nepss  36305  dfon2  36377  relowlpssretop  38126  finxpreclem3  38155  fin2solem  38368  lshpnelb  39865  lshpcmp  39869  lsatssn0  39883  lcvbr3  39904  lsatcv0  39912  lsat0cv  39914  lcvexchlem1  39915  islshpcv  39934  lkrpssN  40044  lkreqN  40051  osumcllem11N  40847  pexmidlem8N  40858  dochsordN  42255  dochsat  42264  dochshpncl  42265  dochexmidlem8  42348  mapdsord  42536  psspwb  43106  xppss12  43107  omssrncard  44388  trelpss  45285  isomenndlem  47366  lvecpsslmod  49445