Theorem tpid3

Description: One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by JJ, 30-Apr-2021)

	Ref	Expression
Hypothesis	tpid3.1	|- C e. _V
Assertion	tpid3	|- C e. { A , B , C }

Proof

Step	Hyp	Ref	Expression
1		tpid3.1	|- C e. _V
2		tpid3g	|- ( C e. _V -> C e. { A , B , C } )
3	1 2	ax-mp	|- C e. { A , B , C }