Definition df-pss 3996

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 30460). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4126). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3993). Other possible definitions are given by dfpss2 4111 and dfpss3 4112. (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 3977	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3976	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2946	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4111  psseq1  4113  psseq2  4114  pssss  4121  pssne  4122  nssinpss  4286  pssdif  4392  0pss  4470  difsnpss  4832  ordelpss  6423  fisseneq  9320  ominf  9321  ominfOLD  9322  f1finf1o  9333  f1finf1oOLD  9334  fofinf1o  9400  inf3lem2  9698  inf3lem4  9700  infeq5  9706  fin23lem31  10412  isf32lem6  10427  ipolt  18605  lssnle  19716  pgpfaclem2  20126  lspsncv0  21171  islbs3  21180  lbsextlem4  21186  lidlnz  21275  filssufilg  23940  alexsubALTlem4  24079  ppiltx  27238  ex-pss  30460  ch0pss  31477  nepss  35680  dfon2  35756  relowlpssretop  37330  finxpreclem3  37359  fin2solem  37566  lshpnelb  38940  lshpcmp  38944  lsatssn0  38958  lcvbr3  38979  lsatcv0  38987  lsat0cv  38989  lcvexchlem1  38990  islshpcv  39009  lkrpssN  39119  lkreqN  39126  osumcllem11N  39923  pexmidlem8N  39934  dochsordN  41331  dochsat  41340  dochshpncl  41341  dochexmidlem8  41424  mapdsord  41612  psspwb  42221  xppss12  42222  omssrncard  43502  trelpss  44424  isomenndlem  46451  lvecpsslmod  48236