Definition df-pss 3931

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 30330). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4062). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3928). Other possible definitions are given by dfpss2 4047 and dfpss3 4048. (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 3912	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3911	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2925	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4047  psseq1  4049  psseq2  4050  pssss  4057  pssne  4058  nssinpss  4226  pssdif  4328  0pss  4406  difsnpss  4767  ordelpss  6348  fisseneq  9180  ominf  9181  ominfOLD  9182  f1finf1o  9192  f1finf1oOLD  9193  fofinf1o  9259  inf3lem2  9558  inf3lem4  9560  infeq5  9566  fin23lem31  10272  isf32lem6  10287  ipolt  18470  lssnle  19580  pgpfaclem2  19990  lspsncv0  21032  islbs3  21041  lbsextlem4  21047  lidlnz  21128  filssufilg  23774  alexsubALTlem4  23913  ppiltx  27063  ex-pss  30330  ch0pss  31347  exsslsb  33565  nepss  35678  dfon2  35753  relowlpssretop  37325  finxpreclem3  37354  fin2solem  37573  lshpnelb  38950  lshpcmp  38954  lsatssn0  38968  lcvbr3  38989  lsatcv0  38997  lsat0cv  38999  lcvexchlem1  39000  islshpcv  39019  lkrpssN  39129  lkreqN  39136  osumcllem11N  39933  pexmidlem8N  39944  dochsordN  41341  dochsat  41350  dochshpncl  41351  dochexmidlem8  41434  mapdsord  41622  psspwb  42189  xppss12  42190  omssrncard  43502  trelpss  44417  isomenndlem  46501  lvecpsslmod  48469