Definition df-pss 3971

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 30447). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4103). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3968). Other possible definitions are given by dfpss2 4088 and dfpss3 4089. (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 3952	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3951	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2940	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 395	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 206	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4088  psseq1  4090  psseq2  4091  pssss  4098  pssne  4099  nssinpss  4267  pssdif  4369  0pss  4447  difsnpss  4807  ordelpss  6412  fisseneq  9293  ominf  9294  ominfOLD  9295  f1finf1o  9305  f1finf1oOLD  9306  fofinf1o  9372  inf3lem2  9669  inf3lem4  9671  infeq5  9677  fin23lem31  10383  isf32lem6  10398  ipolt  18580  lssnle  19692  pgpfaclem2  20102  lspsncv0  21148  islbs3  21157  lbsextlem4  21163  lidlnz  21252  filssufilg  23919  alexsubALTlem4  24058  ppiltx  27220  ex-pss  30447  ch0pss  31464  exsslsb  33647  nepss  35718  dfon2  35793  relowlpssretop  37365  finxpreclem3  37394  fin2solem  37613  lshpnelb  38985  lshpcmp  38989  lsatssn0  39003  lcvbr3  39024  lsatcv0  39032  lsat0cv  39034  lcvexchlem1  39035  islshpcv  39054  lkrpssN  39164  lkreqN  39171  osumcllem11N  39968  pexmidlem8N  39979  dochsordN  41376  dochsat  41385  dochshpncl  41386  dochexmidlem8  41469  mapdsord  41657  psspwb  42267  xppss12  42268  omssrncard  43553  trelpss  44474  isomenndlem  46545  lvecpsslmod  48424