Definition df-pss 2607

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

Assertion

Ref	Expression
df-pss	|- (A C. B <-> (A C_ 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 2594	. 2 wff A C. B
4	1, 2	wss 2593	. . 3 wff A C_ B
5	1, 2	wne 2017	. . 3 wff A =/= B
6	4, 5	wa 240	. 2 wff (A C_ B /\ A =/= B)
7	3, 6	wb 163	1 wff (A C. B <-> (A C_ B /\ A =/= B))

This definition is referenced by:  dfpss2 2694  psseq1 2697  psseq2 2698  pssss 2705  nssinpss 2824  0pss 2910  pssnel 2938  ordelpss 3686  ominf 5622  inf3lem2 5720  inf3lem4 5722  infeq5 5727  sfseqeq 10169  ch0pss 11002  nepss 13820  fundmpss 13836  dfon2lem6 13854  dfon2 13858  top2usne 14898  alexsublem4 15440  filssufil 15571  trelpss 16437  osumcllem11 17374  pexmidlem8 17385

Copyright terms: Public domain