Definition df-pss 3934

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 30357). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4066). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3931). Other possible definitions are given by dfpss2 4051 and dfpss3 4052. (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 3915	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3914	. . 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  4051  psseq1  4053  psseq2  4054  pssss  4061  pssne  4062  nssinpss  4230  pssdif  4332  0pss  4410  difsnpss  4771  ordelpss  6360  fisseneq  9204  ominf  9205  ominfOLD  9206  f1finf1o  9216  f1finf1oOLD  9217  fofinf1o  9283  inf3lem2  9582  inf3lem4  9584  infeq5  9590  fin23lem31  10296  isf32lem6  10311  ipolt  18494  lssnle  19604  pgpfaclem2  20014  lspsncv0  21056  islbs3  21065  lbsextlem4  21071  lidlnz  21152  filssufilg  23798  alexsubALTlem4  23937  ppiltx  27087  ex-pss  30357  ch0pss  31374  exsslsb  33592  nepss  35705  dfon2  35780  relowlpssretop  37352  finxpreclem3  37381  fin2solem  37600  lshpnelb  38977  lshpcmp  38981  lsatssn0  38995  lcvbr3  39016  lsatcv0  39024  lsat0cv  39026  lcvexchlem1  39027  islshpcv  39046  lkrpssN  39156  lkreqN  39163  osumcllem11N  39960  pexmidlem8N  39971  dochsordN  41368  dochsat  41377  dochshpncl  41378  dochexmidlem8  41461  mapdsord  41649  psspwb  42216  xppss12  42217  omssrncard  43529  trelpss  44444  isomenndlem  46528  lvecpsslmod  48496