Theorem tpid1g

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

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

Proof

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