Theorem eltpg

Description: Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014) (Proof shortened by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	eltpg	$$⊢A\in V\to \left(A\in \left\{B,C,D\right\}\leftrightarrow \left(A=B\vee A=C\vee A=D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elprg	$$⊢A\in V\to \left(A\in \left\{B,C\right\}\leftrightarrow \left(A=B\vee A=C\right)\right)$$
2		elsng	$$⊢A\in V\to \left(A\in \left\{D\right\}\leftrightarrow A=D\right)$$
3	1 2	orbi12d	$$⊢A\in V\to \left(\left(A\in \left\{B,C\right\}\vee A\in \left\{D\right\}\right)\leftrightarrow \left(\left(A=B\vee A=C\right)\vee A=D\right)\right)$$
4		df-tp	$$⊢\left\{B,C,D\right\}=\left\{B,C\right\}\cup \left\{D\right\}$$
5	4	eleq2i	$$⊢A\in \left\{B,C,D\right\}\leftrightarrow A\in \left(\left\{B,C\right\}\cup \left\{D\right\}\right)$$
6		elun	$$⊢A\in \left(\left\{B,C\right\}\cup \left\{D\right\}\right)\leftrightarrow \left(A\in \left\{B,C\right\}\vee A\in \left\{D\right\}\right)$$
7	5 6	bitri	$$⊢A\in \left\{B,C,D\right\}\leftrightarrow \left(A\in \left\{B,C\right\}\vee A\in \left\{D\right\}\right)$$
8		df-3or	$$⊢\left(A=B\vee A=C\vee A=D\right)\leftrightarrow \left(\left(A=B\vee A=C\right)\vee A=D\right)$$
9	3 7 8	3bitr4g	$$⊢A\in V\to \left(A\in \left\{B,C,D\right\}\leftrightarrow \left(A=B\vee A=C\vee A=D\right)\right)$$