Step |
Hyp |
Ref |
Expression |
1 |
|
op1stb.1 |
⊢ 𝐴 ∈ V |
2 |
|
op1stb.2 |
⊢ 𝐵 ∈ V |
3 |
1 2
|
dfop |
⊢ 〈 𝐴 , 𝐵 〉 = { { 𝐴 } , { 𝐴 , 𝐵 } } |
4 |
3
|
inteqi |
⊢ ∩ 〈 𝐴 , 𝐵 〉 = ∩ { { 𝐴 } , { 𝐴 , 𝐵 } } |
5 |
|
snex |
⊢ { 𝐴 } ∈ V |
6 |
|
prex |
⊢ { 𝐴 , 𝐵 } ∈ V |
7 |
5 6
|
intpr |
⊢ ∩ { { 𝐴 } , { 𝐴 , 𝐵 } } = ( { 𝐴 } ∩ { 𝐴 , 𝐵 } ) |
8 |
|
snsspr1 |
⊢ { 𝐴 } ⊆ { 𝐴 , 𝐵 } |
9 |
|
df-ss |
⊢ ( { 𝐴 } ⊆ { 𝐴 , 𝐵 } ↔ ( { 𝐴 } ∩ { 𝐴 , 𝐵 } ) = { 𝐴 } ) |
10 |
8 9
|
mpbi |
⊢ ( { 𝐴 } ∩ { 𝐴 , 𝐵 } ) = { 𝐴 } |
11 |
7 10
|
eqtri |
⊢ ∩ { { 𝐴 } , { 𝐴 , 𝐵 } } = { 𝐴 } |
12 |
4 11
|
eqtri |
⊢ ∩ 〈 𝐴 , 𝐵 〉 = { 𝐴 } |
13 |
12
|
inteqi |
⊢ ∩ ∩ 〈 𝐴 , 𝐵 〉 = ∩ { 𝐴 } |
14 |
1
|
intsn |
⊢ ∩ { 𝐴 } = 𝐴 |
15 |
13 14
|
eqtri |
⊢ ∩ ∩ 〈 𝐴 , 𝐵 〉 = 𝐴 |