Definition df-pss 3966

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 29661). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4099). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3964). Other possible definitions are given by dfpss2 4084 and dfpss3 4085. (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 3948	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3947	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2941	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 397	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 205	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is referenced by:  dfpss2  4084  psseq1  4086  psseq2  4087  pssss  4094  pssne  4095  nssinpss  4255  pssdif  4365  0pss  4443  difsnpss  4809  ordelpss  6389  fisseneq  9253  ominf  9254  ominfOLD  9255  f1finf1o  9267  f1finf1oOLD  9268  fofinf1o  9323  inf3lem2  9620  inf3lem4  9622  infeq5  9628  fin23lem31  10334  isf32lem6  10349  ipolt  18484  lssnle  19535  pgpfaclem2  19944  lspsncv0  20747  islbs3  20756  lbsextlem4  20762  lidlnz  20840  filssufilg  23397  alexsubALTlem4  23536  ppiltx  26661  ex-pss  29661  ch0pss  30676  nepss  34625  dfon2  34702  relowlpssretop  36183  finxpreclem3  36212  fin2solem  36412  lshpnelb  37792  lshpcmp  37796  lsatssn0  37810  lcvbr3  37831  lsatcv0  37839  lsat0cv  37841  lcvexchlem1  37842  islshpcv  37861  lkrpssN  37971  lkreqN  37978  osumcllem11N  38775  pexmidlem8N  38786  dochsordN  40183  dochsat  40192  dochshpncl  40193  dochexmidlem8  40276  mapdsord  40464  psspwb  40994  xppss12  40995  omssrncard  42224  trelpss  43147  isomenndlem  45181  lvecpsslmod  47090