Step |
Hyp |
Ref |
Expression |
1 |
|
opeqpr.1 |
|- A e. _V |
2 |
|
opeqpr.2 |
|- B e. _V |
3 |
|
opeqpr.3 |
|- C e. _V |
4 |
|
opeqpr.4 |
|- D e. _V |
5 |
|
eqcom |
|- ( <. A , B >. = { C , D } <-> { C , D } = <. A , B >. ) |
6 |
1 2
|
dfop |
|- <. A , B >. = { { A } , { A , B } } |
7 |
6
|
eqeq2i |
|- ( { C , D } = <. A , B >. <-> { C , D } = { { A } , { A , B } } ) |
8 |
|
snex |
|- { A } e. _V |
9 |
|
prex |
|- { A , B } e. _V |
10 |
3 4 8 9
|
preq12b |
|- ( { C , D } = { { A } , { A , B } } <-> ( ( C = { A } /\ D = { A , B } ) \/ ( C = { A , B } /\ D = { A } ) ) ) |
11 |
5 7 10
|
3bitri |
|- ( <. A , B >. = { C , D } <-> ( ( C = { A } /\ D = { A , B } ) \/ ( C = { A , B } /\ D = { A } ) ) ) |