Step | Hyp | Ref
| Expression |
1 | | vex 2727 |
. . . 4
⊢ 𝑡 ∈ V |
2 | 1 | elima3 4950 |
. . 3
⊢ (𝑡 ∈ (◡(𝐹 ↾ 𝐴) “ 𝐵) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴))) |
3 | 1 | elima3 4950 |
. . . . 5
⊢ (𝑡 ∈ (◡𝐹 “ 𝐵) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹)) |
4 | 3 | anbi1i 454 |
. . . 4
⊢ ((𝑡 ∈ (◡𝐹 “ 𝐵) ∧ 𝑡 ∈ 𝐴) ↔ (∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴)) |
5 | | elin 3303 |
. . . 4
⊢ (𝑡 ∈ ((◡𝐹 “ 𝐵) ∩ 𝐴) ↔ (𝑡 ∈ (◡𝐹 “ 𝐵) ∧ 𝑡 ∈ 𝐴)) |
6 | | vex 2727 |
. . . . . . . . . 10
⊢ 𝑠 ∈ V |
7 | 6, 1 | opelcnv 4783 |
. . . . . . . . 9
⊢
(〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴) ↔ 〈𝑡, 𝑠〉 ∈ (𝐹 ↾ 𝐴)) |
8 | 6 | opelres 4886 |
. . . . . . . . . 10
⊢
(〈𝑡, 𝑠〉 ∈ (𝐹 ↾ 𝐴) ↔ (〈𝑡, 𝑠〉 ∈ 𝐹 ∧ 𝑡 ∈ 𝐴)) |
9 | 6, 1 | opelcnv 4783 |
. . . . . . . . . . 11
⊢
(〈𝑠, 𝑡〉 ∈ ◡𝐹 ↔ 〈𝑡, 𝑠〉 ∈ 𝐹) |
10 | 9 | anbi1i 454 |
. . . . . . . . . 10
⊢
((〈𝑠, 𝑡〉 ∈ ◡𝐹 ∧ 𝑡 ∈ 𝐴) ↔ (〈𝑡, 𝑠〉 ∈ 𝐹 ∧ 𝑡 ∈ 𝐴)) |
11 | 8, 10 | bitr4i 186 |
. . . . . . . . 9
⊢
(〈𝑡, 𝑠〉 ∈ (𝐹 ↾ 𝐴) ↔ (〈𝑠, 𝑡〉 ∈ ◡𝐹 ∧ 𝑡 ∈ 𝐴)) |
12 | 7, 11 | bitri 183 |
. . . . . . . 8
⊢
(〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴) ↔ (〈𝑠, 𝑡〉 ∈ ◡𝐹 ∧ 𝑡 ∈ 𝐴)) |
13 | 12 | anbi2i 453 |
. . . . . . 7
⊢ ((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴)) ↔ (𝑠 ∈ 𝐵 ∧ (〈𝑠, 𝑡〉 ∈ ◡𝐹 ∧ 𝑡 ∈ 𝐴))) |
14 | | anass 399 |
. . . . . . 7
⊢ (((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴) ↔ (𝑠 ∈ 𝐵 ∧ (〈𝑠, 𝑡〉 ∈ ◡𝐹 ∧ 𝑡 ∈ 𝐴))) |
15 | 13, 14 | bitr4i 186 |
. . . . . 6
⊢ ((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴)) ↔ ((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴)) |
16 | 15 | exbii 1592 |
. . . . 5
⊢
(∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴)) ↔ ∃𝑠((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴)) |
17 | | 19.41v 1889 |
. . . . 5
⊢
(∃𝑠((𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴) ↔ (∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴)) |
18 | 16, 17 | bitri 183 |
. . . 4
⊢
(∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴)) ↔ (∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡𝐹) ∧ 𝑡 ∈ 𝐴)) |
19 | 4, 5, 18 | 3bitr4ri 212 |
. . 3
⊢
(∃𝑠(𝑠 ∈ 𝐵 ∧ 〈𝑠, 𝑡〉 ∈ ◡(𝐹 ↾ 𝐴)) ↔ 𝑡 ∈ ((◡𝐹 “ 𝐵) ∩ 𝐴)) |
20 | 2, 19 | bitri 183 |
. 2
⊢ (𝑡 ∈ (◡(𝐹 ↾ 𝐴) “ 𝐵) ↔ 𝑡 ∈ ((◡𝐹 “ 𝐵) ∩ 𝐴)) |
21 | 20 | eqriv 2161 |
1
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) |