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

Metamath Proof Explorer

Theorem imaeqsalvOLD

Description: Obsolete version of ralima as of 14-Aug-2025. Duplicate version of ralima . (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	imaeqsalvOLD	\|- ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) )

Proof

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