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

Metamath Proof Explorer

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 \{C, A, D\}$

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