| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | relxp 5702 | . . . . . 6
⊢ Rel
(𝐶 × 𝐵) | 
| 2 | 1 | rgenw 3064 | . . . . 5
⊢
∀𝑥 ∈
𝐴 Rel (𝐶 × 𝐵) | 
| 3 |  | r19.2z 4494 | . . . . 5
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) → ∃𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) | 
| 4 | 2, 3 | mpan2 691 | . . . 4
⊢ (𝐴 ≠ ∅ →
∃𝑥 ∈ 𝐴 Rel (𝐶 × 𝐵)) | 
| 5 |  | reliin 5826 | . . . 4
⊢
(∃𝑥 ∈
𝐴 Rel (𝐶 × 𝐵) → Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | 
| 6 | 4, 5 | syl 17 | . . 3
⊢ (𝐴 ≠ ∅ → Rel
∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | 
| 7 |  | relxp 5702 | . . 3
⊢ Rel
(𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) | 
| 8 | 6, 7 | jctil 519 | . 2
⊢ (𝐴 ≠ ∅ → (Rel (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) ∧ Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))) | 
| 9 |  | r19.28zv 4500 | . . . . . 6
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵))) | 
| 10 | 9 | bicomd 223 | . . . . 5
⊢ (𝐴 ≠ ∅ → ((𝑦 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵))) | 
| 11 |  | eliin 4995 | . . . . . . 7
⊢ (𝑧 ∈ V → (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵)) | 
| 12 | 11 | elv 3484 | . . . . . 6
⊢ (𝑧 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) | 
| 13 | 12 | anbi2i 623 | . . . . 5
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝑧 ∈ 𝐵)) | 
| 14 |  | opelxp 5720 | . . . . . 6
⊢
(〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵)) | 
| 15 | 14 | ralbii 3092 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐵)) | 
| 16 | 10, 13, 15 | 3bitr4g 314 | . . . 4
⊢ (𝐴 ≠ ∅ → ((𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵))) | 
| 17 |  | opelxp 5720 | . . . 4
⊢
(〈𝑦, 𝑧〉 ∈ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ ∩
𝑥 ∈ 𝐴 𝐵)) | 
| 18 |  | opex 5468 | . . . . 5
⊢
〈𝑦, 𝑧〉 ∈ V | 
| 19 |  | eliin 4995 | . . . . 5
⊢
(〈𝑦, 𝑧〉 ∈ V →
(〈𝑦, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵))) | 
| 20 | 18, 19 | ax-mp 5 | . . . 4
⊢
(〈𝑦, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵) ↔ ∀𝑥 ∈ 𝐴 〈𝑦, 𝑧〉 ∈ (𝐶 × 𝐵)) | 
| 21 | 16, 17, 20 | 3bitr4g 314 | . . 3
⊢ (𝐴 ≠ ∅ →
(〈𝑦, 𝑧〉 ∈ (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) ↔ 〈𝑦, 𝑧〉 ∈ ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵))) | 
| 22 | 21 | eqrelrdv2 5804 | . 2
⊢ (((Rel
(𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) ∧ Rel ∩ 𝑥 ∈ 𝐴 (𝐶 × 𝐵)) ∧ 𝐴 ≠ ∅) → (𝐶 × ∩
𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) | 
| 23 | 8, 22 | mpancom 688 | 1
⊢ (𝐴 ≠ ∅ → (𝐶 × ∩ 𝑥 ∈ 𝐴 𝐵) = ∩
𝑥 ∈ 𝐴 (𝐶 × 𝐵)) |