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 ) ) ) |