Definition df-pss 3968

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 29712). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4101). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3966). Other possible definitions are given by dfpss2 4086 and dfpss3 4087. (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 3950	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3949	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2941	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 397	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 205	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4086  psseq1  4088  psseq2  4089  pssss  4096  pssne  4097  nssinpss  4257  pssdif  4367  0pss  4445  difsnpss  4811  ordelpss  6393  fisseneq  9257  ominf  9258  ominfOLD  9259  f1finf1o  9271  f1finf1oOLD  9272  fofinf1o  9327  inf3lem2  9624  inf3lem4  9626  infeq5  9632  fin23lem31  10338  isf32lem6  10353  ipolt  18488  lssnle  19542  pgpfaclem2  19952  lspsncv0  20759  islbs3  20768  lbsextlem4  20774  lidlnz  20853  filssufilg  23415  alexsubALTlem4  23554  ppiltx  26681  ex-pss  29712  ch0pss  30729  nepss  34718  dfon2  34795  relowlpssretop  36293  finxpreclem3  36322  fin2solem  36522  lshpnelb  37902  lshpcmp  37906  lsatssn0  37920  lcvbr3  37941  lsatcv0  37949  lsat0cv  37951  lcvexchlem1  37952  islshpcv  37971  lkrpssN  38081  lkreqN  38088  osumcllem11N  38885  pexmidlem8N  38896  dochsordN  40293  dochsat  40302  dochshpncl  40303  dochexmidlem8  40386  mapdsord  40574  psspwb  41094  xppss12  41095  omssrncard  42339  trelpss  43262  isomenndlem  45294  lvecpsslmod  47236