Definition df-pss 3926

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 30632). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4058). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3923). Other possible definitions are given by dfpss2 4043 and dfpss3 4044. (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 3907	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3906	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2959	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 399	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 208	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4043  psseq1  4045  psseq2  4046  pssss  4053  pssne  4054  nssinpss  4221  pssdif  4324  0pss  4403  difsnpss  4769  ordelpss  6376  fisseneq  9209  ominf  9210  f1finf1o  9219  fofinf1o  9277  inf3lem2  9586  inf3lem4  9588  infeq5  9594  fin23lem31  10302  isf32lem6  10317  ipolt  18569  lssnle  19716  pgpfaclem2  20126  lspsncv0  21218  islbs3  21227  lbsextlem4  21233  lidlnz  21314  filssufilg  23973  alexsubALTlem4  24112  ppiltx  27243  ex-pss  30632  ch0pss  31650  exsslsb  33896  nepss  36073  dfon2  36145  relowlpssretop  37863  finxpreclem3  37892  fin2solem  38110  lshpnelb  39613  lshpcmp  39617  lsatssn0  39631  lcvbr3  39652  lsatcv0  39660  lsat0cv  39662  lcvexchlem1  39663  islshpcv  39682  lkrpssN  39792  lkreqN  39799  osumcllem11N  40595  pexmidlem8N  40606  dochsordN  42003  dochsat  42012  dochshpncl  42013  dochexmidlem8  42096  mapdsord  42284  psspwb  42852  xppss12  42853  omssrncard  44121  trelpss  45035  isomenndlem  47109  lvecpsslmod  49134