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

Proof

Step Hyp Ref Expression
1 imaeqexov.1 
 |-  ( x = ( y F z ) -> ( ph <-> ps ) )
2 df-rex 
 |-  ( E. x e. ( F " ( B X. C ) ) ph <-> E. 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 anbi1d 
 |-  ( ( 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 r19.41v 
 |-  ( E. z e. C ( x = ( y F z ) /\ ph ) <-> ( E. z e. C x = ( y F z ) /\ ph ) )
6 5 rexbii 
 |-  ( E. 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 ) )
7 r19.41v 
 |-  ( E. 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 ) )
8 6 7 bitr2i 
 |-  ( ( E. 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 ) )
9 4 8 bitrdi 
 |-  ( ( 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 ) ) )
10 9 exbidv 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( E. x ( x e. ( F " ( B X. C ) ) /\ ph ) <-> E. x E. y e. B E. z e. C ( x = ( y F z ) /\ ph ) ) )
11 rexcom4 
 |-  ( E. y e. B E. x E. z e. C ( x = ( y F z ) /\ ph ) <-> E. x E. y e. B E. z e. C ( x = ( y F z ) /\ ph ) )
12 rexcom4 
 |-  ( E. z e. C E. x ( x = ( y F z ) /\ ph ) <-> E. x E. z e. C ( x = ( y F z ) /\ ph ) )
13 ovex 
 |-  ( y F z ) e. _V
14 13 1 ceqsexv 
 |-  ( E. x ( x = ( y F z ) /\ ph ) <-> ps )
15 14 rexbii 
 |-  ( E. z e. C E. x ( x = ( y F z ) /\ ph ) <-> E. z e. C ps )
16 12 15 bitr3i 
 |-  ( E. x E. z e. C ( x = ( y F z ) /\ ph ) <-> E. z e. C ps )
17 16 rexbii 
 |-  ( E. y e. B E. x E. z e. C ( x = ( y F z ) /\ ph ) <-> E. y e. B E. z e. C ps )
18 11 17 bitr3i 
 |-  ( E. x E. y e. B E. z e. C ( x = ( y F z ) /\ ph ) <-> E. y e. B E. z e. C ps )
19 10 18 bitrdi 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( E. x ( x e. ( F " ( B X. C ) ) /\ ph ) <-> E. y e. B E. z e. C ps ) )
20 2 19 bitrid 
 |-  ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( E. x e. ( F " ( B X. C ) ) ph <-> E. y e. B E. z e. C ps ) )