Definition df-pss 3946

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 30355). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4078). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3943). Other possible definitions are given by dfpss2 4063 and dfpss3 4064. (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 3927	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3926	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2932	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4063  psseq1  4065  psseq2  4066  pssss  4073  pssne  4074  nssinpss  4242  pssdif  4344  0pss  4422  difsnpss  4783  ordelpss  6380  fisseneq  9263  ominf  9264  ominfOLD  9265  f1finf1o  9275  f1finf1oOLD  9276  fofinf1o  9342  inf3lem2  9641  inf3lem4  9643  infeq5  9649  fin23lem31  10355  isf32lem6  10370  ipolt  18543  lssnle  19653  pgpfaclem2  20063  lspsncv0  21105  islbs3  21114  lbsextlem4  21120  lidlnz  21201  filssufilg  23847  alexsubALTlem4  23986  ppiltx  27137  ex-pss  30355  ch0pss  31372  exsslsb  33582  nepss  35681  dfon2  35756  relowlpssretop  37328  finxpreclem3  37357  fin2solem  37576  lshpnelb  38948  lshpcmp  38952  lsatssn0  38966  lcvbr3  38987  lsatcv0  38995  lsat0cv  38997  lcvexchlem1  38998  islshpcv  39017  lkrpssN  39127  lkreqN  39134  osumcllem11N  39931  pexmidlem8N  39942  dochsordN  41339  dochsat  41348  dochshpncl  41349  dochexmidlem8  41432  mapdsord  41620  psspwb  42225  xppss12  42226  omssrncard  43511  trelpss  44427  isomenndlem  46507  lvecpsslmod  48431