Step |
Hyp |
Ref |
Expression |
1 |
|
op1stb.1 |
|- A e. _V |
2 |
|
op1stb.2 |
|- B e. _V |
3 |
1 2
|
dfop |
|- <. A , B >. = { { A } , { A , B } } |
4 |
3
|
inteqi |
|- |^| <. A , B >. = |^| { { A } , { A , B } } |
5 |
|
snex |
|- { A } e. _V |
6 |
|
prex |
|- { A , B } e. _V |
7 |
5 6
|
intpr |
|- |^| { { A } , { A , B } } = ( { A } i^i { A , B } ) |
8 |
|
snsspr1 |
|- { A } C_ { A , B } |
9 |
|
df-ss |
|- ( { A } C_ { A , B } <-> ( { A } i^i { A , B } ) = { A } ) |
10 |
8 9
|
mpbi |
|- ( { A } i^i { A , B } ) = { A } |
11 |
7 10
|
eqtri |
|- |^| { { A } , { A , B } } = { A } |
12 |
4 11
|
eqtri |
|- |^| <. A , B >. = { A } |
13 |
12
|
inteqi |
|- |^| |^| <. A , B >. = |^| { A } |
14 |
1
|
intsn |
|- |^| { A } = A |
15 |
13 14
|
eqtri |
|- |^| |^| <. A , B >. = A |