Definition df-pss 3903

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 28668). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4032). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3901). Other possible definitions are given by dfpss2 4017 and dfpss3 4018. (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 3885	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3884	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2943	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 399	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4017  psseq1  4019  psseq2  4020  pssss  4027  pssne  4028  nssinpss  4188  pssdif  4298  0pss  4376  difsnpss  4737  ordelpss  6276  fisseneq  8937  ominf  8938  f1finf1o  8950  fofinf1o  8999  inf3lem2  9292  inf3lem4  9294  infeq5  9300  fin23lem31  10005  isf32lem6  10020  ipolt  18143  lssnle  19170  pgpfaclem2  19575  lspsncv0  20298  islbs3  20307  lbsextlem4  20313  lidlnz  20387  filssufilg  22945  alexsubALTlem4  23084  ppiltx  26206  ex-pss  28668  ch0pss  29683  nepss  33539  dfon2  33649  relowlpssretop  35441  finxpreclem3  35470  fin2solem  35669  lshpnelb  36904  lshpcmp  36908  lsatssn0  36922  lcvbr3  36943  lsatcv0  36951  lsat0cv  36953  lcvexchlem1  36954  islshpcv  36973  lkrpssN  37083  lkreqN  37090  osumcllem11N  37886  pexmidlem8N  37897  dochsordN  39294  dochsat  39303  dochshpncl  39304  dochexmidlem8  39387  mapdsord  39575  psspwb  40101  xppss12  40102  trelpss  41935  isomenndlem  43931  lvecpsslmod  45709