Definition df-pss 2107

Description: Define proper subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. Other possible definitions are given by dfpss2 2185 and dfpss3 2186.

Assertion

Ref	Expression
df-pss	⊢ (A ⊂ B ↔ (A ⊆ B ⋀ A ≠ B))

Detailed syntax breakdown of Definition df-pss

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wpss 2100	. 2 wff A ⊂ B
4	1, 2	wss 2099	. . 3 wff A ⊆ B
5	1, 2	wne 1628	. . 3 wff A ≠ B
6	4, 5	wa 221	. 2 wff (A ⊆ B ⋀ A ≠ B)
7	3, 6	wb 144	1 wff (A ⊂ B ↔ (A ⊆ B ⋀ A ≠ B))

This definition is referenced by:  dfpss2 2185  psseq1 2187  psseq2 2188  pssss 2195  0pss 2361  pssnel 2384  ordelpss 3003  ominf 4675  inf3lem2 4759  inf3lem4 4761  infeq5 4766  ch0pss 9645  sfseqeq 10824  top2usne 11051  alexsublem4 11499  filssufil 11656

Copyright terms: Public domain