Metamath Proof Explorer


Theorem f1oeq23

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

Ref Expression
Assertion f1oeq23 ( ( 𝐴 = 𝐵𝐶 = 𝐷 ) → ( 𝐹 : 𝐴1-1-onto𝐶𝐹 : 𝐵1-1-onto𝐷 ) )

Proof

Step Hyp Ref Expression
1 f1oeq2 ( 𝐴 = 𝐵 → ( 𝐹 : 𝐴1-1-onto𝐶𝐹 : 𝐵1-1-onto𝐶 ) )
2 f1oeq3 ( 𝐶 = 𝐷 → ( 𝐹 : 𝐵1-1-onto𝐶𝐹 : 𝐵1-1-onto𝐷 ) )
3 1 2 sylan9bb ( ( 𝐴 = 𝐵𝐶 = 𝐷 ) → ( 𝐹 : 𝐴1-1-onto𝐶𝐹 : 𝐵1-1-onto𝐷 ) )