Definition df-pss 3556

Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. For example, {1, 2} ⊊ {1, 2, 3} (ex-pss 26677). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 3669). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3554). Other possible definitions are given by dfpss2 3654 and dfpss3 3655. (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 3541	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3540	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2780	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 383	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 195	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  3654  psseq1  3656  psseq2  3657  pssss  3664  pssne  3665  nssinpss  3818  pssdif  3899  0pss  3965  difsnpss  4279  ordelpss  5668  fisseneq  8056  ominf  8057  f1finf1o  8072  fofinf1o  8126  inf3lem2  8409  inf3lem4  8411  infeq5  8417  fin23lem31  9048  isf32lem6  9063  ipolt  16982  lssnle  17910  pgpfaclem2  18304  lspsncv0  18967  islbs3  18976  lbsextlem4  18982  lidlnz  19049  filssufilg  21525  alexsubALTlem4  21664  ppiltx  24703  ex-pss  26677  ch0pss  27688  nepss  30854  dfon2  30941  relowlpssretop  32388  finxpreclem3  32406  fin2solem  32565  lshpnelb  33289  lshpcmp  33293  lsatssn0  33307  lcvbr3  33328  lsatcv0  33336  lsat0cv  33338  lcvexchlem1  33339  islshpcv  33358  lkrpssN  33468  lkreqN  33475  osumcllem11N  34270  pexmidlem8N  34281  dochsordN  35681  dochsat  35690  dochshpncl  35691  dochexmidlem8  35774  mapdsord  35962  trelpss  37680  isomenndlem  39420  lvecpsslmod  42090