Step |
Hyp |
Ref |
Expression |
1 |
|
elun |
|- ( X e. ( { A } u. ( { B , C , D } u. { E , F , G } ) ) <-> ( X e. { A } \/ X e. ( { B , C , D } u. { E , F , G } ) ) ) |
2 |
|
elsng |
|- ( X e. V -> ( X e. { A } <-> X = A ) ) |
3 |
|
elun |
|- ( X e. ( { B , C , D } u. { E , F , G } ) <-> ( X e. { B , C , D } \/ X e. { E , F , G } ) ) |
4 |
|
eltpg |
|- ( X e. V -> ( X e. { B , C , D } <-> ( X = B \/ X = C \/ X = D ) ) ) |
5 |
|
eltpg |
|- ( X e. V -> ( X e. { E , F , G } <-> ( X = E \/ X = F \/ X = G ) ) ) |
6 |
4 5
|
orbi12d |
|- ( X e. V -> ( ( X e. { B , C , D } \/ X e. { E , F , G } ) <-> ( ( X = B \/ X = C \/ X = D ) \/ ( X = E \/ X = F \/ X = G ) ) ) ) |
7 |
3 6
|
bitrid |
|- ( X e. V -> ( X e. ( { B , C , D } u. { E , F , G } ) <-> ( ( X = B \/ X = C \/ X = D ) \/ ( X = E \/ X = F \/ X = G ) ) ) ) |
8 |
2 7
|
orbi12d |
|- ( X e. V -> ( ( X e. { A } \/ X e. ( { B , C , D } u. { E , F , G } ) ) <-> ( X = A \/ ( ( X = B \/ X = C \/ X = D ) \/ ( X = E \/ X = F \/ X = G ) ) ) ) ) |
9 |
1 8
|
bitrid |
|- ( X e. V -> ( X e. ( { A } u. ( { B , C , D } u. { E , F , G } ) ) <-> ( X = A \/ ( ( X = B \/ X = C \/ X = D ) \/ ( X = E \/ X = F \/ X = G ) ) ) ) ) |