Metamath Proof Explorer

Theorem eltpi

Description: A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion eltpi 
|- ( A e. { B , C , D } -> ( A = B \/ A = C \/ A = D ) )

Proof

Step Hyp Ref Expression
1 eltpg 
 |-  ( A e. { B , C , D } -> ( A e. { B , C , D } <-> ( A = B \/ A = C \/ A = D ) ) )
2 1 ibi 
 |-  ( A e. { B , C , D } -> ( A = B \/ A = C \/ A = D ) )