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 ψ