Definition df-pss 4014

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 31029). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4030). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3896). Other possible definitions are given by dfpss2 4015 and dfpss3 4016. (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 4013	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3895	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2955	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 401	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is used by:  dfpss2  4015  psseq1  4017  psseq2  4018  pssss  4025  pssne  4026  nssinpss  4212  pssdif  4316  0pss  4359  difsnpss  4769  ordelpss  6390  fisseneq  9254  ominf  9255  f1finf1o  9264  fofinf1o  9321  inf3lem2  9630  inf3lem4  9632  infeq5  9638  fin23lem31  10421  isf32lem6  10436  ipolt  18709  lssnle  19888  pgpfaclem2  20298  lspsncv0  21424  islbs3  21433  lbsextlem4  21439  lidlnz  21530  filssufilg  24230  alexsubALTlem4  24369  ppiltx  27504  ex-pss  31029  ch0pss  32047  exsslsb  34271  nepss  36525  dfon2  36596  relowlpssretop  38330  finxpreclem3  38359  fin2solem  38572  lshpnelb  40084  lshpcmp  40088  lsatssn0  40102  lcvbr3  40123  lsatcv0  40131  lsat0cv  40133  lcvexchlem1  40134  islshpcv  40153  lkrpssN  40263  lkreqN  40270  osumcllem11N  41066  pexmidlem8N  41077  dochsordN  42474  dochsat  42483  dochshpncl  42484  dochexmidlem8  42567  mapdsord  42755  psspwb  43325  xppss12  43326  omssrncard  44583  trelpss  45479  isomenndlem  47582  lvecpsslmod  49661