Metamath Proof Explorer

Theorem imaeqalov

Description: Substitute an operation value into a universal quantifier over an image. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Hypothesis imaeqexov.1 ⊢ x = y F z → φ ↔ ψ
Assertion imaeqalov ⊢ F Fn A ∧ B × C ⊆ A → ∀ x ∈ F B × C φ ↔ ∀ y ∈ B ∀ z ∈ C ψ

Proof

Step Hyp Ref Expression
1 imaeqexov.1 ⊢ x = y F z → φ ↔ ψ
2 df-ral ⊢ ∀ x ∈ F B × C φ ↔ ∀ x x ∈ F B × C → φ
3 ovelimab ⊢ F Fn A ∧ B × C ⊆ A → x ∈ F B × C ↔ ∃ y ∈ B ∃ z ∈ C x = y F z
4 3 imbi1d ⊢ F Fn A ∧ B × C ⊆ A → x ∈ F B × C → φ ↔ ∃ y ∈ B ∃ z ∈ C x = y F z → φ
5 4 albidv ⊢ F Fn A ∧ B × C ⊆ A → ∀ x x ∈ F B × C → φ ↔ ∀ x ∃ y ∈ B ∃ z ∈ C x = y F z → φ
6 2 5 bitrid ⊢ F Fn A ∧ B × C ⊆ A → ∀ x ∈ F B × C φ ↔ ∀ x ∃ y ∈ B ∃ z ∈ C x = y F z → φ
7 ralcom4 ⊢ ∀ y ∈ B ∀ x ∀ z ∈ C x = y F z → φ ↔ ∀ x ∀ y ∈ B ∀ z ∈ C x = y F z → φ
8 r19.23v ⊢ ∀ z ∈ C x = y F z → φ ↔ ∃ z ∈ C x = y F z → φ
9 8 ralbii ⊢ ∀ y ∈ B ∀ z ∈ C x = y F z → φ ↔ ∀ y ∈ B ∃ z ∈ C x = y F z → φ
10 r19.23v ⊢ ∀ y ∈ B ∃ z ∈ C x = y F z → φ ↔ ∃ y ∈ B ∃ z ∈ C x = y F z → φ
11 9 10 bitri ⊢ ∀ y ∈ B ∀ z ∈ C x = y F z → φ ↔ ∃ y ∈ B ∃ z ∈ C x = y F z → φ
12 11 albii ⊢ ∀ x ∀ y ∈ B ∀ z ∈ C x = y F z → φ ↔ ∀ x ∃ y ∈ B ∃ z ∈ C x = y F z → φ
13 7 12 bitri ⊢ ∀ y ∈ B ∀ x ∀ z ∈ C x = y F z → φ ↔ ∀ x ∃ y ∈ B ∃ z ∈ C x = y F z → φ
14 ralcom4 ⊢ ∀ z ∈ C ∀ x x = y F z → φ ↔ ∀ x ∀ z ∈ C x = y F z → φ
15 ovex ⊢ y F z ∈ V
16 15 1 ceqsalv ⊢ ∀ x x = y F z → φ ↔ ψ
17 16 ralbii ⊢ ∀ z ∈ C ∀ x x = y F z → φ ↔ ∀ z ∈ C ψ
18 14 17 bitr3i ⊢ ∀ x ∀ z ∈ C x = y F z → φ ↔ ∀ z ∈ C ψ
19 18 ralbii ⊢ ∀ y ∈ B ∀ x ∀ z ∈ C x = y F z → φ ↔ ∀ y ∈ B ∀ z ∈ C ψ
20 13 19 bitr3i ⊢ ∀ x ∃ y ∈ B ∃ z ∈ C x = y F z → φ ↔ ∀ y ∈ B ∀ z ∈ C ψ
21 6 20 bitrdi ⊢ F Fn A ∧ B × C ⊆ A → ∀ x ∈ F B × C φ ↔ ∀ y ∈ B ∀ z ∈ C ψ