Metamath Proof Explorer

Theorem eltpg

Description: Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014) (Proof shortened by Mario Carneiro, 11-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 elprg 
 |-  ( A e. V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
2 elsng 
 |-  ( A e. V -> ( A e. { D } <-> A = D ) )
3 1 2 orbi12d 
 |-  ( A e. V -> ( ( A e. { B , C } \/ A e. { D } ) <-> ( ( A = B \/ A = C ) \/ A = D ) ) )
4 df-tp 
 |-  { B , C , D } = ( { B , C } u. { D } )
5 4 eleq2i 
 |-  ( A e. { B , C , D } <-> A e. ( { B , C } u. { D } ) )
6 elun 
 |-  ( A e. ( { B , C } u. { D } ) <-> ( A e. { B , C } \/ A e. { D } ) )
7 5 6 bitri 
 |-  ( A e. { B , C , D } <-> ( A e. { B , C } \/ A e. { D } ) )
8 df-3or 
 |-  ( ( A = B \/ A = C \/ A = D ) <-> ( ( A = B \/ A = C ) \/ A = D ) )
9 3 7 8 3bitr4g 
 |-  ( A e. V -> ( A e. { B , C , D } <-> ( A = B \/ A = C \/ A = D ) ) )