| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | inpreima 7083 | . . . . . . . . 9
⊢ (Fun
𝐹 → (◡𝐹 “ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) = ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵))) | 
| 2 |  | imaeq2 6073 | . . . . . . . . . 10
⊢
((⦋𝑦 /
𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ → (◡𝐹 “ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) = (◡𝐹 “ ∅)) | 
| 3 |  | ima0 6094 | . . . . . . . . . 10
⊢ (◡𝐹 “ ∅) = ∅ | 
| 4 | 2, 3 | eqtrdi 2792 | . . . . . . . . 9
⊢
((⦋𝑦 /
𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ → (◡𝐹 “ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) = ∅) | 
| 5 | 1, 4 | sylan9req 2797 | . . . . . . . 8
⊢ ((Fun
𝐹 ∧
(⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵)) = ∅) | 
| 6 | 5 | ex 412 | . . . . . . 7
⊢ (Fun
𝐹 →
((⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ → ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵)) = ∅)) | 
| 7 |  | csbima12 6096 | . . . . . . . . . 10
⊢
⦋𝑦 /
𝑥⦌(◡𝐹 “ 𝐵) = (⦋𝑦 / 𝑥⦌◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) | 
| 8 |  | csbconstg 3917 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌◡𝐹 = ◡𝐹) | 
| 9 | 8 | elv 3484 | . . . . . . . . . . 11
⊢
⦋𝑦 /
𝑥⦌◡𝐹 = ◡𝐹 | 
| 10 | 9 | imaeq1i 6074 | . . . . . . . . . 10
⊢
(⦋𝑦 /
𝑥⦌◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) = (◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) | 
| 11 | 7, 10 | eqtri 2764 | . . . . . . . . 9
⊢
⦋𝑦 /
𝑥⦌(◡𝐹 “ 𝐵) = (◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) | 
| 12 |  | csbima12 6096 | . . . . . . . . . 10
⊢
⦋𝑧 /
𝑥⦌(◡𝐹 “ 𝐵) = (⦋𝑧 / 𝑥⦌◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵) | 
| 13 |  | csbconstg 3917 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ V →
⦋𝑧 / 𝑥⦌◡𝐹 = ◡𝐹) | 
| 14 | 13 | elv 3484 | . . . . . . . . . . 11
⊢
⦋𝑧 /
𝑥⦌◡𝐹 = ◡𝐹 | 
| 15 | 14 | imaeq1i 6074 | . . . . . . . . . 10
⊢
(⦋𝑧 /
𝑥⦌◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵) = (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵) | 
| 16 | 12, 15 | eqtri 2764 | . . . . . . . . 9
⊢
⦋𝑧 /
𝑥⦌(◡𝐹 “ 𝐵) = (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵) | 
| 17 | 11, 16 | ineq12i 4217 | . . . . . . . 8
⊢
(⦋𝑦 /
𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵)) | 
| 18 | 17 | eqeq1i 2741 | . . . . . . 7
⊢
((⦋𝑦 /
𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅ ↔ ((◡𝐹 “ ⦋𝑦 / 𝑥⦌𝐵) ∩ (◡𝐹 “ ⦋𝑧 / 𝑥⦌𝐵)) = ∅) | 
| 19 | 6, 18 | imbitrrdi 252 | . . . . . 6
⊢ (Fun
𝐹 →
((⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ → (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅)) | 
| 20 | 19 | orim2d 968 | . . . . 5
⊢ (Fun
𝐹 → ((𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅))) | 
| 21 | 20 | ralimdv 3168 | . . . 4
⊢ (Fun
𝐹 → (∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅))) | 
| 22 | 21 | ralimdv 3168 | . . 3
⊢ (Fun
𝐹 → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅))) | 
| 23 |  | disjors 5125 | . . 3
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) | 
| 24 |  | disjors 5125 | . . 3
⊢
(Disj 𝑥
∈ 𝐴 (◡𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(◡𝐹 “ 𝐵) ∩ ⦋𝑧 / 𝑥⦌(◡𝐹 “ 𝐵)) = ∅)) | 
| 25 | 22, 23, 24 | 3imtr4g 296 | . 2
⊢ (Fun
𝐹 → (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵))) | 
| 26 | 25 | imp 406 | 1
⊢ ((Fun
𝐹 ∧ Disj 𝑥 ∈ 𝐴 𝐵) → Disj 𝑥 ∈ 𝐴 (◡𝐹 “ 𝐵)) |