Definition df-pss 3922

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 30894). Note that ¬ 𝐴 ⊊ 𝐴 (proved in pssirr 4054). Contrast this relationship with the relationship 𝐴 ⊆ 𝐵 (as defined in df-ss 3919). Other possible definitions are given by dfpss2 4039 and dfpss3 4040. (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 3903	. 2 wff 𝐴 ⊊ 𝐵
4	1, 2	wss 3902	. . 3 wff 𝐴 ⊆ 𝐵
5	1, 2	wne 2957	. . 3 wff 𝐴 ≠ 𝐵
6	4, 5	wa 401	. 2 wff (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵)
7	3, 6	wb 209	1 wff (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))

This definition is used by:  dfpss2  4039  psseq1  4041  psseq2  4042  pssss  4049  pssne  4050  nssinpss  4216  pssdif  4320  0pss  4363  difsnpss  4773  ordelpss  6389  fisseneq  9236  ominf  9237  f1finf1o  9246  fofinf1o  9302  inf3lem2  9611  inf3lem4  9613  infeq5  9619  fin23lem31  10348  isf32lem6  10363  ipolt  18627  lssnle  19802  pgpfaclem2  20212  lspsncv0  21334  islbs3  21343  lbsextlem4  21349  lidlnz  21440  filssufilg  24138  alexsubALTlem4  24277  ppiltx  27411  ex-pss  30894  ch0pss  31912  exsslsb  34094  nepss  36284  dfon2  36356  relowlpssretop  38105  finxpreclem3  38134  fin2solem  38347  lshpnelb  39844  lshpcmp  39848  lsatssn0  39862  lcvbr3  39883  lsatcv0  39891  lsat0cv  39893  lcvexchlem1  39894  islshpcv  39913  lkrpssN  40023  lkreqN  40030  osumcllem11N  40826  pexmidlem8N  40837  dochsordN  42234  dochsat  42243  dochshpncl  42244  dochexmidlem8  42327  mapdsord  42515  psspwb  43085  xppss12  43086  omssrncard  44367  trelpss  45264  isomenndlem  47345  lvecpsslmod  49424