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

Metamath Proof Explorer

Theorem imaeqsexvOLD

Description: Obsolete version of rexima as of 14-Aug-2025. Duplicate version of rexima . (Contributed by Scott Fenton, 27-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		imaeqsexvOLD.1	\|- ( x = ( F ` y ) -> ( ph <-> ps ) )
2		df-rex	\|- ( E. x e. ( F " B ) ph <-> E. x ( x e. ( F " B ) /\ ph ) )
3		fvelimab	\|- ( ( F Fn A /\ B C_ A ) -> ( x e. ( F " B ) <-> E. y e. B ( F ` y ) = x ) )
4	3	anbi1d	\|- ( ( F Fn A /\ B C_ A ) -> ( ( x e. ( F " B ) /\ ph ) <-> ( E. y e. B ( F ` y ) = x /\ ph ) ) )
5	4	exbidv	\|- ( ( F Fn A /\ B C_ A ) -> ( E. x ( x e. ( F " B ) /\ ph ) <-> E. x ( E. y e. B ( F ` y ) = x /\ ph ) ) )
6	2 5	bitrid	\|- ( ( F Fn A /\ B C_ A ) -> ( E. x e. ( F " B ) ph <-> E. x ( E. y e. B ( F ` y ) = x /\ ph ) ) )
7		rexcom4	\|- ( E. y e. B E. x ( ( F ` y ) = x /\ ph ) <-> E. x E. y e. B ( ( F ` y ) = x /\ ph ) )
8		eqcom	\|- ( ( F ` y ) = x <-> x = ( F ` y ) )
9	8	anbi1i	\|- ( ( ( F ` y ) = x /\ ph ) <-> ( x = ( F ` y ) /\ ph ) )
10	9	exbii	\|- ( E. x ( ( F ` y ) = x /\ ph ) <-> E. x ( x = ( F ` y ) /\ ph ) )
11		fvex	\|- ( F ` y ) e. _V
12	11 1	ceqsexv	\|- ( E. x ( x = ( F ` y ) /\ ph ) <-> ps )
13	10 12	bitri	\|- ( E. x ( ( F ` y ) = x /\ ph ) <-> ps )
14	13	rexbii	\|- ( E. y e. B E. x ( ( F ` y ) = x /\ ph ) <-> E. y e. B ps )
15		r19.41v	\|- ( E. y e. B ( ( F ` y ) = x /\ ph ) <-> ( E. y e. B ( F ` y ) = x /\ ph ) )
16	15	exbii	\|- ( E. x E. y e. B ( ( F ` y ) = x /\ ph ) <-> E. x ( E. y e. B ( F ` y ) = x /\ ph ) )
17	7 14 16	3bitr3ri	\|- ( E. x ( E. y e. B ( F ` y ) = x /\ ph ) <-> E. y e. B ps )
18	6 17	bitrdi	\|- ( ( F Fn A /\ B C_ A ) -> ( E. x e. ( F " B ) ph <-> E. y e. B ps ) )