This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-pss

Description: Define proper subclass (or strict subclass) relationship between two classes. Definition 5.9 of TakeutiZaring p. 17. For example, { 1 , 2 } C. { 1 , 2 , 3 } ( ex-pss ). Note that -. A C. A (proved in pssirr ). Contrast this relationship with the relationship A C_ B (as defined in df-ss ). Other possible definitions are given by dfpss2 and dfpss3 . (Contributed by NM, 7-Feb-1996)

		Ref	Expression
	Assertion	df-pss	⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	wpss	⊢ 𝐴 ⊊ 𝐵
3	0 1	wss	⊢ 𝐴 ⊆ 𝐵
4	0 1	wne	⊢ 𝐴 ≠ 𝐵
5	3 4	wa	⊢ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 )
6	2 5	wb	⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵 ) )