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

Metamath Proof Explorer

Theorem eltpi

Description: A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	eltpi	$⊢ A \in \{B, C, D\} \to (A = B \lor A = C \lor A = D)$

Step	Hyp	Ref	Expression
1		eltpg	$⊢ A \in \{B, C, D\} \to (A \in \{B, C, D\} \leftrightarrow (A = B \lor A = C \lor A = D))$
2	1	ibi	$⊢ A \in \{B, C, D\} \to (A = B \lor A = C \lor A = D)$