Theorem tpid2g

Description: Closed theorem form of tpid2 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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