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

Metamath Proof Explorer

Theorem foeq123d

Description: Equality deduction for onto functions. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses f1eq123d.1 ⊢ ( 𝜑 → 𝐹 = 𝐺 )
f1eq123d.2 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
f1eq123d.3 ⊢ ( 𝜑 → 𝐶 = 𝐷 )
Assertion foeq123d ( 𝜑 → ( 𝐹 : 𝐴 –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 f1eq123d.1 ⊢ ( 𝜑 → 𝐹 = 𝐺 )
2 f1eq123d.2 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
3 f1eq123d.3 ⊢ ( 𝜑 → 𝐶 = 𝐷 )
4 foeq1 ⊢ ( 𝐹 = 𝐺 → ( 𝐹 : 𝐴 –onto→ 𝐶 ↔ 𝐺 : 𝐴 –onto→ 𝐶 ) )
5 1 4 syl ⊢ ( 𝜑 → ( 𝐹 : 𝐴 –onto→ 𝐶 ↔ 𝐺 : 𝐴 –onto→ 𝐶 ) )
6 foeq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐺 : 𝐴 –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐶 ) )
7 2 6 syl ⊢ ( 𝜑 → ( 𝐺 : 𝐴 –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐶 ) )
8 foeq3 ⊢ ( 𝐶 = 𝐷 → ( 𝐺 : 𝐵 –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐷 ) )
9 3 8 syl ⊢ ( 𝜑 → ( 𝐺 : 𝐵 –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐷 ) )
10 5 7 9 3bitrd ⊢ ( 𝜑 → ( 𝐹 : 𝐴 –onto→ 𝐶 ↔ 𝐺 : 𝐵 –onto→ 𝐷 ) )