Definition df-pss 3906

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 28792). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4035). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3904). Other possible definitions are given by dfpss2 4020 and dfpss3 4021. (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 3888	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3887	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2943	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 396	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 205	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4020  psseq1  4022  psseq2  4023  pssss  4030  pssne  4031  nssinpss  4190  pssdif  4300  0pss  4378  difsnpss  4740  ordelpss  6294  fisseneq  9034  ominf  9035  f1finf1o  9046  fofinf1o  9094  inf3lem2  9387  inf3lem4  9389  infeq5  9395  fin23lem31  10099  isf32lem6  10114  ipolt  18253  lssnle  19280  pgpfaclem2  19685  lspsncv0  20408  islbs3  20417  lbsextlem4  20423  lidlnz  20499  filssufilg  23062  alexsubALTlem4  23201  ppiltx  26326  ex-pss  28792  ch0pss  29807  nepss  33662  dfon2  33768  relowlpssretop  35535  finxpreclem3  35564  fin2solem  35763  lshpnelb  36998  lshpcmp  37002  lsatssn0  37016  lcvbr3  37037  lsatcv0  37045  lsat0cv  37047  lcvexchlem1  37048  islshpcv  37067  lkrpssN  37177  lkreqN  37184  osumcllem11N  37980  pexmidlem8N  37991  dochsordN  39388  dochsat  39397  dochshpncl  39398  dochexmidlem8  39481  mapdsord  39669  psspwb  40203  xppss12  40204  omssrncard  41147  trelpss  42073  isomenndlem  44068  lvecpsslmod  45848