Step |
Hyp |
Ref |
Expression |
1 |
|
brprop.a |
|- ( ph -> A e. V ) |
2 |
|
brprop.b |
|- ( ph -> B e. W ) |
3 |
|
brprop.c |
|- ( ph -> C e. V ) |
4 |
|
brprop.d |
|- ( ph -> D e. W ) |
5 |
|
df-pr |
|- { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } ) |
6 |
5
|
breqi |
|- ( X { <. A , B >. , <. C , D >. } Y <-> X ( { <. A , B >. } u. { <. C , D >. } ) Y ) |
7 |
|
brun |
|- ( X ( { <. A , B >. } u. { <. C , D >. } ) Y <-> ( X { <. A , B >. } Y \/ X { <. C , D >. } Y ) ) |
8 |
6 7
|
bitri |
|- ( X { <. A , B >. , <. C , D >. } Y <-> ( X { <. A , B >. } Y \/ X { <. C , D >. } Y ) ) |
9 |
|
brsnop |
|- ( ( A e. V /\ B e. W ) -> ( X { <. A , B >. } Y <-> ( X = A /\ Y = B ) ) ) |
10 |
1 2 9
|
syl2anc |
|- ( ph -> ( X { <. A , B >. } Y <-> ( X = A /\ Y = B ) ) ) |
11 |
|
brsnop |
|- ( ( C e. V /\ D e. W ) -> ( X { <. C , D >. } Y <-> ( X = C /\ Y = D ) ) ) |
12 |
3 4 11
|
syl2anc |
|- ( ph -> ( X { <. C , D >. } Y <-> ( X = C /\ Y = D ) ) ) |
13 |
10 12
|
orbi12d |
|- ( ph -> ( ( X { <. A , B >. } Y \/ X { <. C , D >. } Y ) <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) ) ) ) |
14 |
8 13
|
syl5bb |
|- ( ph -> ( X { <. A , B >. , <. C , D >. } Y <-> ( ( X = A /\ Y = B ) \/ ( X = C /\ Y = D ) ) ) ) |