Metamath Proof Explorer


Theorem imaeqexov

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

Ref Expression
Hypothesis imaeqexov.1 x = y F z φ ψ
Assertion imaeqexov 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-rex 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 anbi1d F Fn A B × C A x F B × C φ y B z C x = y F z φ
5 r19.41v z C x = y F z φ z C x = y F z φ
6 5 rexbii y B z C x = y F z φ y B z C x = y F z φ
7 r19.41v y B z C x = y F z φ y B z C x = y F z φ
8 6 7 bitr2i y B z C x = y F z φ y B z C x = y F z φ
9 4 8 bitrdi F Fn A B × C A x F B × C φ y B z C x = y F z φ
10 9 exbidv F Fn A B × C A x x F B × C φ x y B z C x = y F z φ
11 rexcom4 y B x z C x = y F z φ x y B z C x = y F z φ
12 rexcom4 z C x x = y F z φ x z C x = y F z φ
13 ovex y F z V
14 13 1 ceqsexv x x = y F z φ ψ
15 14 rexbii z C x x = y F z φ z C ψ
16 12 15 bitr3i x z C x = y F z φ z C ψ
17 16 rexbii y B x z C x = y F z φ y B z C ψ
18 11 17 bitr3i x y B z C x = y F z φ y B z C ψ
19 10 18 bitrdi F Fn A B × C A x x F B × C φ y B z C ψ
20 2 19 bitrid F Fn A B × C A x F B × C φ y B z C ψ