Metamath Proof Explorer

Theorem tpid2

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 tpid2.1 
|- B e. _V
Assertion tpid2 
|- B e. { A , B , C }

Proof

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