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

Metamath Proof Explorer

Theorem rexima

Description: Existential 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 rexima 
|- ( ( F Fn A /\ B C_ A ) -> ( E. x e. ( F " B ) ph <-> E. y e. B ps ) )

Proof

Step Hyp Ref Expression
1 ralima.x 
 |-  ( x = ( F ` y ) -> ( ph <-> ps ) )
2 1 notbid 
 |-  ( x = ( F ` y ) -> ( -. ph <-> -. ps ) )
3 2 ralima 
 |-  ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) -. ph <-> A. y e. B -. ps ) )
4 3 notbid 
 |-  ( ( F Fn A /\ B C_ A ) -> ( -. A. x e. ( F " B ) -. ph <-> -. A. y e. B -. ps ) )
5 dfrex2 
 |-  ( E. x e. ( F " B ) ph <-> -. A. x e. ( F " B ) -. ph )
6 dfrex2 
 |-  ( E. y e. B ps <-> -. A. y e. B -. ps )
7 4 5 6 3bitr4g 
 |-  ( ( F Fn A /\ B C_ A ) -> ( E. x e. ( F " B ) ph <-> E. y e. B ps ) )