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

Metamath Proof Explorer

Theorem f1oabexgOLD

Description: Obsolete version of f1oabexg as of 9-Jun-2025. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	f1oabexg.1	\|- F = { f \| ( f : A -1-1-onto-> B /\ ph ) }
	Assertion	f1oabexgOLD	\|- ( ( A e. C /\ B e. D ) -> F e. _V )

Proof

Step	Hyp	Ref	Expression
1		f1oabexg.1	\|- F = { f \| ( f : A -1-1-onto-> B /\ ph ) }
2		f1of	\|- ( f : A -1-1-onto-> B -> f : A --> B )
3	2	anim1i	\|- ( ( f : A -1-1-onto-> B /\ ph ) -> ( f : A --> B /\ ph ) )
4	3	ss2abi	\|- { f \| ( f : A -1-1-onto-> B /\ ph ) } C_ { f \| ( f : A --> B /\ ph ) }
5		eqid	\|- { f \| ( f : A --> B /\ ph ) } = { f \| ( f : A --> B /\ ph ) }
6	5	fabexg	\|- ( ( A e. C /\ B e. D ) -> { f \| ( f : A --> B /\ ph ) } e. _V )
7		ssexg	\|- ( ( { f \| ( f : A -1-1-onto-> B /\ ph ) } C_ { f \| ( f : A --> B /\ ph ) } /\ { f \| ( f : A --> B /\ ph ) } e. _V ) -> { f \| ( f : A -1-1-onto-> B /\ ph ) } e. _V )
8	4 6 7	sylancr	\|- ( ( A e. C /\ B e. D ) -> { f \| ( f : A -1-1-onto-> B /\ ph ) } e. _V )
9	1 8	eqeltrid	\|- ( ( A e. C /\ B e. D ) -> F e. _V )