Theorem fneq1

Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Assertion	fneq1	⊢ ( 𝐹 = 𝐺 → ( 𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		funeq	⊢ ( 𝐹 = 𝐺 → ( Fun 𝐹 ↔ Fun 𝐺 ) )
2		dmeq	⊢ ( 𝐹 = 𝐺 → dom 𝐹 = dom 𝐺 )
3	2	eqeq1d	⊢ ( 𝐹 = 𝐺 → ( dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴 ) )
4	1 3	anbi12d	⊢ ( 𝐹 = 𝐺 → ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ↔ ( Fun 𝐺 ∧ dom 𝐺 = 𝐴 ) ) )
5		df-fn	⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
6		df-fn	⊢ ( 𝐺 Fn 𝐴 ↔ ( Fun 𝐺 ∧ dom 𝐺 = 𝐴 ) )
7	4 5 6	3bitr4g	⊢ ( 𝐹 = 𝐺 → ( 𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴 ) )