Definition df-pss 3982

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

This definition is referenced by:  dfpss2  4097  psseq1  4099  psseq2  4100  pssss  4107  pssne  4108  nssinpss  4272  pssdif  4374  0pss  4452  difsnpss  4811  ordelpss  6413  fisseneq  9290  ominf  9291  ominfOLD  9292  f1finf1o  9302  f1finf1oOLD  9303  fofinf1o  9369  inf3lem2  9666  inf3lem4  9668  infeq5  9674  fin23lem31  10380  isf32lem6  10395  ipolt  18592  lssnle  19706  pgpfaclem2  20116  lspsncv0  21165  islbs3  21174  lbsextlem4  21180  lidlnz  21269  filssufilg  23934  alexsubALTlem4  24073  ppiltx  27234  ex-pss  30456  ch0pss  31473  nepss  35697  dfon2  35773  relowlpssretop  37346  finxpreclem3  37375  fin2solem  37592  lshpnelb  38965  lshpcmp  38969  lsatssn0  38983  lcvbr3  39004  lsatcv0  39012  lsat0cv  39014  lcvexchlem1  39015  islshpcv  39034  lkrpssN  39144  lkreqN  39151  osumcllem11N  39948  pexmidlem8N  39959  dochsordN  41356  dochsat  41365  dochshpncl  41366  dochexmidlem8  41449  mapdsord  41637  psspwb  42245  xppss12  42246  omssrncard  43529  trelpss  44450  isomenndlem  46485  lvecpsslmod  48352