Theorem f1eq1

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997)

	Ref	Expression
Assertion	f1eq1	⊢ ( 𝐹 = 𝐺 → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐺 : 𝐴 –1-1→ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		feq1	⊢ ( 𝐹 = 𝐺 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐺 : 𝐴 ⟶ 𝐵 ) )
2		cnveq	⊢ ( 𝐹 = 𝐺 → ◡ 𝐹 = ◡ 𝐺 )
3	2	funeqd	⊢ ( 𝐹 = 𝐺 → ( Fun ◡ 𝐹 ↔ Fun ◡ 𝐺 ) )
4	1 3	anbi12d	⊢ ( 𝐹 = 𝐺 → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) ↔ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐺 ) ) )
5		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
6		df-f1	⊢ ( 𝐺 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐺 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐺 ) )
7	4 5 6	3bitr4g	⊢ ( 𝐹 = 𝐺 → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ 𝐺 : 𝐴 –1-1→ 𝐵 ) )