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 ⊢FFnA∧B⊆A→∃x∈FBφ↔∃y∈Bψ

Proof

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