Metamath Proof Explorer

Theorem f1oeq23

Description: Equality theorem for one-to-one onto functions. (Contributed by FL, 14-Jul-2012)

		Ref	Expression
	Assertion	f1oeq23	\|- ( ( A = B /\ C = D ) -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> D ) )

Step	Hyp	Ref	Expression
1		f1oeq2	\|- ( A = B -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> C ) )
2		f1oeq3	\|- ( C = D -> ( F : B -1-1-onto-> C <-> F : B -1-1-onto-> D ) )
3	1 2	sylan9bb	\|- ( ( A = B /\ C = D ) -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> D ) )

Step

Hyp

Ref

Expression

 |-  ( A = B -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> C ) )

 |-  ( C = D -> ( F : B -1-1-onto-> C <-> F : B -1-1-onto-> D ) )

1 2

 |-  ( ( A = B /\ C = D ) -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> D ) )