Definition df-pss 3964

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 29610). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4097). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3962). Other possible definitions are given by dfpss2 4082 and dfpss3 4083. (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 3946	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3945	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2940	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 396	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 205	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4082  psseq1  4084  psseq2  4085  pssss  4092  pssne  4093  nssinpss  4253  pssdif  4363  0pss  4441  difsnpss  4804  ordelpss  6382  fisseneq  9242  ominf  9243  ominfOLD  9244  f1finf1o  9256  f1finf1oOLD  9257  fofinf1o  9312  inf3lem2  9608  inf3lem4  9610  infeq5  9616  fin23lem31  10322  isf32lem6  10337  ipolt  18472  lssnle  19508  pgpfaclem2  19913  lspsncv0  20710  islbs3  20719  lbsextlem4  20725  lidlnz  20801  filssufilg  23346  alexsubALTlem4  23485  ppiltx  26610  ex-pss  29610  ch0pss  30625  nepss  34581  dfon2  34658  relowlpssretop  36113  finxpreclem3  36142  fin2solem  36342  lshpnelb  37723  lshpcmp  37727  lsatssn0  37741  lcvbr3  37762  lsatcv0  37770  lsat0cv  37772  lcvexchlem1  37773  islshpcv  37792  lkrpssN  37902  lkreqN  37909  osumcllem11N  38706  pexmidlem8N  38717  dochsordN  40114  dochsat  40123  dochshpncl  40124  dochexmidlem8  40207  mapdsord  40395  psspwb  40925  xppss12  40926  omssrncard  42126  trelpss  43049  isomenndlem  45083  lvecpsslmod  46900