Definition df-pss 3590

Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 27285). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 3707). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3588). Other possible definitions are given by dfpss2 3692 and dfpss3 3693. (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 3575	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3574	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2794	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 384	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 196	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  3692  psseq1  3694  psseq2  3695  pssss  3702  pssne  3703  nssinpss  3856  pssdif  3945  0pss  4013  difsnpss  4338  ordelpss  5751  fisseneq  8171  ominf  8172  f1finf1o  8187  fofinf1o  8241  inf3lem2  8526  inf3lem4  8528  infeq5  8534  fin23lem31  9165  isf32lem6  9180  ipolt  17159  lssnle  18087  pgpfaclem2  18481  lspsncv0  19146  islbs3  19155  lbsextlem4  19161  lidlnz  19228  filssufilg  21715  alexsubALTlem4  21854  ppiltx  24903  ex-pss  27285  ch0pss  28304  nepss  31599  dfon2  31697  relowlpssretop  33212  finxpreclem3  33230  fin2solem  33395  lshpnelb  34271  lshpcmp  34275  lsatssn0  34289  lcvbr3  34310  lsatcv0  34318  lsat0cv  34320  lcvexchlem1  34321  islshpcv  34340  lkrpssN  34450  lkreqN  34457  osumcllem11N  35252  pexmidlem8N  35263  dochsordN  36663  dochsat  36672  dochshpncl  36673  dochexmidlem8  36756  mapdsord  36944  trelpss  38659  isomenndlem  40744  lvecpsslmod  42296