| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssint 4964 | . . 3
⊢ (𝐶 ⊆ ∩ (𝐹
“ 𝐵) ↔
∀𝑦 ∈ (𝐹 “ 𝐵)𝐶 ⊆ 𝑦) | 
| 2 |  | df-ral 3062 | . . 3
⊢
(∀𝑦 ∈
(𝐹 “ 𝐵)𝐶 ⊆ 𝑦 ↔ ∀𝑦(𝑦 ∈ (𝐹 “ 𝐵) → 𝐶 ⊆ 𝑦)) | 
| 3 | 1, 2 | bitri 275 | . 2
⊢ (𝐶 ⊆ ∩ (𝐹
“ 𝐵) ↔
∀𝑦(𝑦 ∈ (𝐹 “ 𝐵) → 𝐶 ⊆ 𝑦)) | 
| 4 |  | fvelimab 6981 | . . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦)) | 
| 5 | 4 | imbi1d 341 | . . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → ((𝑦 ∈ (𝐹 “ 𝐵) → 𝐶 ⊆ 𝑦) ↔ (∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦))) | 
| 6 | 5 | albidv 1920 | . . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑦(𝑦 ∈ (𝐹 “ 𝐵) → 𝐶 ⊆ 𝑦) ↔ ∀𝑦(∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦))) | 
| 7 |  | ralcom4 3286 | . . . 4
⊢
(∀𝑥 ∈
𝐵 ∀𝑦((𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦) ↔ ∀𝑦∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦)) | 
| 8 |  | eqcom 2744 | . . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑦 ↔ 𝑦 = (𝐹‘𝑥)) | 
| 9 | 8 | imbi1i 349 | . . . . . . 7
⊢ (((𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦) ↔ (𝑦 = (𝐹‘𝑥) → 𝐶 ⊆ 𝑦)) | 
| 10 | 9 | albii 1819 | . . . . . 6
⊢
(∀𝑦((𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦) ↔ ∀𝑦(𝑦 = (𝐹‘𝑥) → 𝐶 ⊆ 𝑦)) | 
| 11 |  | fvex 6919 | . . . . . . 7
⊢ (𝐹‘𝑥) ∈ V | 
| 12 |  | sseq2 4010 | . . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ (𝐹‘𝑥))) | 
| 13 | 11, 12 | ceqsalv 3521 | . . . . . 6
⊢
(∀𝑦(𝑦 = (𝐹‘𝑥) → 𝐶 ⊆ 𝑦) ↔ 𝐶 ⊆ (𝐹‘𝑥)) | 
| 14 | 10, 13 | bitri 275 | . . . . 5
⊢
(∀𝑦((𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦) ↔ 𝐶 ⊆ (𝐹‘𝑥)) | 
| 15 | 14 | ralbii 3093 | . . . 4
⊢
(∀𝑥 ∈
𝐵 ∀𝑦((𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦) ↔ ∀𝑥 ∈ 𝐵 𝐶 ⊆ (𝐹‘𝑥)) | 
| 16 |  | r19.23v 3183 | . . . . 5
⊢
(∀𝑥 ∈
𝐵 ((𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦) ↔ (∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦)) | 
| 17 | 16 | albii 1819 | . . . 4
⊢
(∀𝑦∀𝑥 ∈ 𝐵 ((𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦) ↔ ∀𝑦(∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦)) | 
| 18 | 7, 15, 17 | 3bitr3ri 302 | . . 3
⊢
(∀𝑦(∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦 → 𝐶 ⊆ 𝑦) ↔ ∀𝑥 ∈ 𝐵 𝐶 ⊆ (𝐹‘𝑥)) | 
| 19 | 6, 18 | bitrdi 287 | . 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑦(𝑦 ∈ (𝐹 “ 𝐵) → 𝐶 ⊆ 𝑦) ↔ ∀𝑥 ∈ 𝐵 𝐶 ⊆ (𝐹‘𝑥))) | 
| 20 | 3, 19 | bitrid 283 | 1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ ∩ (𝐹 “ 𝐵) ↔ ∀𝑥 ∈ 𝐵 𝐶 ⊆ (𝐹‘𝑥))) |