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 ) -> ( ph <-> ps ) )
Assertion imaeqalov 
|- ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( A. x e. ( F " ( B X. C ) ) ph <-> A. y e. B A. z e. C ps ) )

Proof

Step Hyp Ref Expression
1 imaeqexov.1 
 |-  ( x = ( y F z ) -> ( ph <-> ps ) )
2 df-ral 
 |-  ( A. x e. ( F " ( B X. C ) ) ph <-> A. x ( x e. ( F " ( B X. C ) ) -> ph ) )
3 ovelimab 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( x e. ( F " ( B X. C ) ) <-> E. y e. B E. z e. C x = ( y F z ) ) )
4 3 imbi1d 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( ( x e. ( F " ( B X. C ) ) -> ph ) <-> ( E. y e. B E. z e. C x = ( y F z ) -> ph ) ) )
5 4 albidv 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( A. x ( x e. ( F " ( B X. C ) ) -> ph ) <-> A. x ( E. y e. B E. z e. C x = ( y F z ) -> ph ) ) )
6 2 5 bitrid 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( A. x e. ( F " ( B X. C ) ) ph <-> A. x ( E. y e. B E. z e. C x = ( y F z ) -> ph ) ) )
7 ralcom4 
 |-  ( A. y e. B A. x A. z e. C ( x = ( y F z ) -> ph ) <-> A. x A. y e. B A. z e. C ( x = ( y F z ) -> ph ) )
8 r19.23v 
 |-  ( A. z e. C ( x = ( y F z ) -> ph ) <-> ( E. z e. C x = ( y F z ) -> ph ) )
9 8 ralbii 
 |-  ( A. y e. B A. z e. C ( x = ( y F z ) -> ph ) <-> A. y e. B ( E. z e. C x = ( y F z ) -> ph ) )
10 r19.23v 
 |-  ( A. y e. B ( E. z e. C x = ( y F z ) -> ph ) <-> ( E. y e. B E. z e. C x = ( y F z ) -> ph ) )
11 9 10 bitri 
 |-  ( A. y e. B A. z e. C ( x = ( y F z ) -> ph ) <-> ( E. y e. B E. z e. C x = ( y F z ) -> ph ) )
12 11 albii 
 |-  ( A. x A. y e. B A. z e. C ( x = ( y F z ) -> ph ) <-> A. x ( E. y e. B E. z e. C x = ( y F z ) -> ph ) )
13 7 12 bitri 
 |-  ( A. y e. B A. x A. z e. C ( x = ( y F z ) -> ph ) <-> A. x ( E. y e. B E. z e. C x = ( y F z ) -> ph ) )
14 ralcom4 
 |-  ( A. z e. C A. x ( x = ( y F z ) -> ph ) <-> A. x A. z e. C ( x = ( y F z ) -> ph ) )
15 ovex 
 |-  ( y F z ) e. _V
16 15 1 ceqsalv 
 |-  ( A. x ( x = ( y F z ) -> ph ) <-> ps )
17 16 ralbii 
 |-  ( A. z e. C A. x ( x = ( y F z ) -> ph ) <-> A. z e. C ps )
18 14 17 bitr3i 
 |-  ( A. x A. z e. C ( x = ( y F z ) -> ph ) <-> A. z e. C ps )
19 18 ralbii 
 |-  ( A. y e. B A. x A. z e. C ( x = ( y F z ) -> ph ) <-> A. y e. B A. z e. C ps )
20 13 19 bitr3i 
 |-  ( A. x ( E. y e. B E. z e. C x = ( y F z ) -> ph ) <-> A. y e. B A. z e. C ps )
21 6 20 bitrdi 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( A. x e. ( F " ( B X. C ) ) ph <-> A. y e. B A. z e. C ps ) )