Definition df-pss 3905

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 30486). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4036). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3902). Other possible definitions are given by dfpss2 4021 and dfpss3 4022. (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 3886	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3885	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2930	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4021  psseq1  4023  psseq2  4024  pssss  4031  pssne  4032  nssinpss  4197  pssdif  4299  0pss  4377  difsnpss  4742  ordelpss  6340  fisseneq  9162  ominf  9163  f1finf1o  9172  fofinf1o  9231  inf3lem2  9539  inf3lem4  9541  infeq5  9547  fin23lem31  10254  isf32lem6  10269  ipolt  18490  lssnle  19638  pgpfaclem2  20048  lspsncv0  21133  islbs3  21142  lbsextlem4  21148  lidlnz  21229  filssufilg  23864  alexsubALTlem4  24003  ppiltx  27128  ex-pss  30486  ch0pss  31504  exsslsb  33729  nepss  35888  dfon2  35960  relowlpssretop  37668  finxpreclem3  37697  fin2solem  37915  lshpnelb  39418  lshpcmp  39422  lsatssn0  39436  lcvbr3  39457  lsatcv0  39465  lsat0cv  39467  lcvexchlem1  39468  islshpcv  39487  lkrpssN  39597  lkreqN  39604  osumcllem11N  40400  pexmidlem8N  40411  dochsordN  41808  dochsat  41817  dochshpncl  41818  dochexmidlem8  41901  mapdsord  42089  psspwb  42657  xppss12  42658  omssrncard  43955  trelpss  44869  isomenndlem  46946  lvecpsslmod  48971