| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | relcnv 6122 | . 2
⊢ Rel ◡∩ 𝑥 ∈ 𝐴 𝐵 | 
| 2 |  | relcnv 6122 | . . . . . . 7
⊢ Rel ◡𝐵 | 
| 3 |  | df-rel 5692 | . . . . . . 7
⊢ (Rel
◡𝐵 ↔ ◡𝐵 ⊆ (V × V)) | 
| 4 | 2, 3 | mpbi 230 | . . . . . 6
⊢ ◡𝐵 ⊆ (V × V) | 
| 5 | 4 | rgenw 3065 | . . . . 5
⊢
∀𝑥 ∈
𝐴 ◡𝐵 ⊆ (V × V) | 
| 6 |  | r19.2z 4495 | . . . . 5
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) → ∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) | 
| 7 | 5, 6 | mpan2 691 | . . . 4
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) | 
| 8 |  | iinss 5056 | . . . 4
⊢
(∃𝑥 ∈
𝐴 ◡𝐵 ⊆ (V × V) → ∩ 𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) | 
| 9 | 7, 8 | syl 17 | . . 3
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) | 
| 10 |  | df-rel 5692 | . . 3
⊢ (Rel
∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∩
𝑥 ∈ 𝐴 ◡𝐵 ⊆ (V × V)) | 
| 11 | 9, 10 | sylibr 234 | . 2
⊢ (𝐴 ≠ ∅ → Rel
∩ 𝑥 ∈ 𝐴 ◡𝐵) | 
| 12 |  | opex 5469 | . . . . 5
⊢
〈𝑏, 𝑎〉 ∈ V | 
| 13 |  | eliin 4996 | . . . . 5
⊢
(〈𝑏, 𝑎〉 ∈ V →
(〈𝑏, 𝑎〉 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵)) | 
| 14 | 12, 13 | ax-mp 5 | . . . 4
⊢
(〈𝑏, 𝑎〉 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵) | 
| 15 |  | vex 3484 | . . . . 5
⊢ 𝑎 ∈ V | 
| 16 |  | vex 3484 | . . . . 5
⊢ 𝑏 ∈ V | 
| 17 | 15, 16 | opelcnv 5892 | . . . 4
⊢
(〈𝑎, 𝑏〉 ∈ ◡∩ 𝑥 ∈ 𝐴 𝐵 ↔ 〈𝑏, 𝑎〉 ∈ ∩ 𝑥 ∈ 𝐴 𝐵) | 
| 18 |  | opex 5469 | . . . . . 6
⊢
〈𝑎, 𝑏〉 ∈ V | 
| 19 |  | eliin 4996 | . . . . . 6
⊢
(〈𝑎, 𝑏〉 ∈ V →
(〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑎, 𝑏〉 ∈ ◡𝐵)) | 
| 20 | 18, 19 | ax-mp 5 | . . . . 5
⊢
(〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑎, 𝑏〉 ∈ ◡𝐵) | 
| 21 | 15, 16 | opelcnv 5892 | . . . . . 6
⊢
(〈𝑎, 𝑏〉 ∈ ◡𝐵 ↔ 〈𝑏, 𝑎〉 ∈ 𝐵) | 
| 22 | 21 | ralbii 3093 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 〈𝑎, 𝑏〉 ∈ ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵) | 
| 23 | 20, 22 | bitri 275 | . . . 4
⊢
(〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑏, 𝑎〉 ∈ 𝐵) | 
| 24 | 14, 17, 23 | 3bitr4i 303 | . . 3
⊢
(〈𝑎, 𝑏〉 ∈ ◡∩ 𝑥 ∈ 𝐴 𝐵 ↔ 〈𝑎, 𝑏〉 ∈ ∩ 𝑥 ∈ 𝐴 ◡𝐵) | 
| 25 | 24 | eqrelriv 5799 | . 2
⊢ ((Rel
◡∩
𝑥 ∈ 𝐴 𝐵 ∧ Rel ∩ 𝑥 ∈ 𝐴 ◡𝐵) → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) | 
| 26 | 1, 11, 25 | sylancr 587 | 1
⊢ (𝐴 ≠ ∅ → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) |