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 30507). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4056). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3919). Other possible definitions are given by dfpss2 4041 and dfpss3 4042. (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 2933	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4041  psseq1  4043  psseq2  4044  pssss  4051  pssne  4052  nssinpss  4220  pssdif  4322  0pss  4400  difsnpss  4764  ordelpss  6346  fisseneq  9167  ominf  9168  f1finf1o  9177  fofinf1o  9236  inf3lem2  9542  inf3lem4  9544  infeq5  9550  fin23lem31  10257  isf32lem6  10272  ipolt  18462  lssnle  19607  pgpfaclem2  20017  lspsncv0  21105  islbs3  21114  lbsextlem4  21120  lidlnz  21201  filssufilg  23859  alexsubALTlem4  23998  ppiltx  27147  ex-pss  30507  ch0pss  31524  exsslsb  33755  nepss  35914  dfon2  35986  relowlpssretop  37571  finxpreclem3  37600  fin2solem  37809  lshpnelb  39312  lshpcmp  39316  lsatssn0  39330  lcvbr3  39351  lsatcv0  39359  lsat0cv  39361  lcvexchlem1  39362  islshpcv  39381  lkrpssN  39491  lkreqN  39498  osumcllem11N  40294  pexmidlem8N  40305  dochsordN  41702  dochsat  41711  dochshpncl  41712  dochexmidlem8  41795  mapdsord  41983  psspwb  42552  xppss12  42553  omssrncard  43848  trelpss  44762  isomenndlem  46841  lvecpsslmod  48820