Metamath Proof Explorer

Theorem imaeqsexv

Description: Substitute a function value into an existential quantifier over an image. (Contributed by Scott Fenton, 27-Sep-2024)

Ref Expression
Hypothesis imaeqsex.1 ⊢ x = F ⁡ y → φ ↔ ψ
Assertion imaeqsexv ⊢ F Fn A ∧ B ⊆ A → ∃ x ∈ F B φ ↔ ∃ y ∈ B ψ

Proof

Step Hyp Ref Expression
1 imaeqsex.1 ⊢ x = F ⁡ y → φ ↔ ψ
2 df-rex ⊢ ∃ x ∈ F B φ ↔ ∃ x x ∈ F B ∧ φ
3 fvelimab ⊢ F Fn A ∧ B ⊆ A → x ∈ F B ↔ ∃ y ∈ B F ⁡ y = x
4 3 anbi1d ⊢ F Fn A ∧ B ⊆ A → x ∈ F B ∧ φ ↔ ∃ y ∈ B F ⁡ y = x ∧ φ
5 4 exbidv ⊢ F Fn A ∧ B ⊆ A → ∃ x x ∈ F B ∧ φ ↔ ∃ x ∃ y ∈ B F ⁡ y = x ∧ φ
6 2 5 syl5bb ⊢ F Fn A ∧ B ⊆ A → ∃ x ∈ F B φ ↔ ∃ x ∃ y ∈ B F ⁡ y = x ∧ φ
7 rexcom4 ⊢ ∃ y ∈ B ∃ x F ⁡ y = x ∧ φ ↔ ∃ x ∃ y ∈ B F ⁡ y = x ∧ φ
8 eqcom ⊢ F ⁡ y = x ↔ x = F ⁡ y
9 8 anbi1i ⊢ F ⁡ y = x ∧ φ ↔ x = F ⁡ y ∧ φ
10 9 exbii ⊢ ∃ x F ⁡ y = x ∧ φ ↔ ∃ x x = F ⁡ y ∧ φ
11 fvex ⊢ F ⁡ y ∈ V
12 11 1 ceqsexv ⊢ ∃ x x = F ⁡ y ∧ φ ↔ ψ
13 10 12 bitri ⊢ ∃ x F ⁡ y = x ∧ φ ↔ ψ
14 13 rexbii ⊢ ∃ y ∈ B ∃ x F ⁡ y = x ∧ φ ↔ ∃ y ∈ B ψ
15 r19.41v ⊢ ∃ y ∈ B F ⁡ y = x ∧ φ ↔ ∃ y ∈ B F ⁡ y = x ∧ φ
16 15 exbii ⊢ ∃ x ∃ y ∈ B F ⁡ y = x ∧ φ ↔ ∃ x ∃ y ∈ B F ⁡ y = x ∧ φ
17 7 14 16 3bitr3ri ⊢ ∃ x ∃ y ∈ B F ⁡ y = x ∧ φ ↔ ∃ y ∈ B ψ
18 6 17 bitrdi ⊢ F Fn A ∧ B ⊆ A → ∃ x ∈ F B φ ↔ ∃ y ∈ B ψ