Theorem reximaOLD

Description: Obsolete version of rexima as of 14-Aug-2025. (Contributed by Stefan O'Rear, 21-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		reximaOLD.x	|- ( x = ( F ` y ) -> ( ph <-> ps ) )
2		fvexd	|- ( ( ( F Fn A /\ B C_ A ) /\ y e. B ) -> ( F ` y ) e. _V )
3		fvelimab	|- ( ( F Fn A /\ B C_ A ) -> ( x e. ( F " B ) <-> E. y e. B ( F ` y ) = x ) )
4		eqcom	|- ( ( F ` y ) = x <-> x = ( F ` y ) )
5	4	rexbii	|- ( E. y e. B ( F ` y ) = x <-> E. y e. B x = ( F ` y ) )
6	3 5	bitrdi	|- ( ( F Fn A /\ B C_ A ) -> ( x e. ( F " B ) <-> E. y e. B x = ( F ` y ) ) )
7	1	adantl	|- ( ( ( F Fn A /\ B C_ A ) /\ x = ( F ` y ) ) -> ( ph <-> ps ) )
8	2 6 7	rexxfr2d	|- ( ( F Fn A /\ B C_ A ) -> ( E. x e. ( F " B ) ph <-> E. y e. B ps ) )