Metamath Proof Explorer

Theorem tpid1

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

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

Proof

Step Hyp Ref Expression
1 tpid1.1 
 |-  A e. _V
2 eqid 
 |-  A = A
3 2 3mix1i 
 |-  ( A = A \/ A = B \/ A = C )
4 1 eltp 
 |-  ( A e. { A , B , C } <-> ( A = A \/ A = B \/ A = C ) )
5 3 4 mpbir 
 |-  A e. { A , B , C }