Definition df-pss 3623

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

This definition is referenced by:  dfpss2  3725  psseq1  3727  psseq2  3728  pssss  3735  pssne  3736  nssinpss  3889  pssdif  3978  0pss  4046  difsnpss  4370  ordelpss  5789  fisseneq  8212  ominf  8213  f1finf1o  8228  fofinf1o  8282  inf3lem2  8564  inf3lem4  8566  infeq5  8572  fin23lem31  9203  isf32lem6  9218  ipolt  17206  lssnle  18133  pgpfaclem2  18527  lspsncv0  19194  islbs3  19203  lbsextlem4  19209  lidlnz  19276  filssufilg  21762  alexsubALTlem4  21901  ppiltx  24948  ex-pss  27415  ch0pss  28432  nepss  31725  dfon2  31821  relowlpssretop  33342  finxpreclem3  33360  fin2solem  33525  lshpnelb  34589  lshpcmp  34593  lsatssn0  34607  lcvbr3  34628  lsatcv0  34636  lsat0cv  34638  lcvexchlem1  34639  islshpcv  34658  lkrpssN  34768  lkreqN  34775  osumcllem11N  35570  pexmidlem8N  35581  dochsordN  36980  dochsat  36989  dochshpncl  36990  dochexmidlem8  37073  mapdsord  37261  trelpss  38976  isomenndlem  41065  lvecpsslmod  42621