This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ralima

Description: Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025)

Ref Expression
Hypothesis ralima.x 
|- ( x = ( F ` y ) -> ( ph <-> ps ) )
Assertion ralima 
|- ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) )

Proof

Step Hyp Ref Expression
1 ralima.x 
 |-  ( x = ( F ` y ) -> ( ph <-> ps ) )
2 fnfun 
 |-  ( F Fn A -> Fun F )
3 2 funfnd 
 |-  ( F Fn A -> F Fn dom F )
4 fndm 
 |-  ( F Fn A -> dom F = A )
5 4 sseq2d 
 |-  ( F Fn A -> ( B C_ dom F <-> B C_ A ) )
6 5 biimpar 
 |-  ( ( F Fn A /\ B C_ A ) -> B C_ dom F )
7 fvexd 
 |-  ( ( ( F Fn dom F /\ B C_ dom F ) /\ y e. B ) -> ( F ` y ) e. _V )
8 fvelimab 
 |-  ( ( F Fn dom F /\ B C_ dom F ) -> ( x e. ( F " B ) <-> E. y e. B ( F ` y ) = x ) )
9 eqcom 
 |-  ( ( F ` y ) = x <-> x = ( F ` y ) )
10 9 rexbii 
 |-  ( E. y e. B ( F ` y ) = x <-> E. y e. B x = ( F ` y ) )
11 8 10 bitrdi 
 |-  ( ( F Fn dom F /\ B C_ dom F ) -> ( x e. ( F " B ) <-> E. y e. B x = ( F ` y ) ) )
12 1 adantl 
 |-  ( ( ( F Fn dom F /\ B C_ dom F ) /\ x = ( F ` y ) ) -> ( ph <-> ps ) )
13 7 11 12 ralxfr2d 
 |-  ( ( F Fn dom F /\ B C_ dom F ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) )
14 3 6 13 syl2an2r 
 |-  ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) )