Theorem tpid3g

Description: Closed theorem form of tpid3 . (Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by JJ, 30-Apr-2021)

	Ref	Expression
Assertion	tpid3g	$$⊢A\in B\to A\in \left\{C,D,A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A=A$$
2	1	3mix3i	$$⊢\left(A=C\vee A=D\vee A=A\right)$$
3		eltpg	$$⊢A\in B\to \left(A\in \left\{C,D,A\right\}\leftrightarrow \left(A=C\vee A=D\vee A=A\right)\right)$$
4	2 3	mpbiri	$$⊢A\in B\to A\in \left\{C,D,A\right\}$$