Theorem fneq2

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

	Ref	Expression
Assertion	fneq2	⊢ ( 𝐴 = 𝐵 → ( 𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq2	⊢ ( 𝐴 = 𝐵 → ( dom 𝐹 = 𝐴 ↔ dom 𝐹 = 𝐵 ) )
2	1	anbi2d	⊢ ( 𝐴 = 𝐵 → ( ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) ) )
3		df-fn	⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
4		df-fn	⊢ ( 𝐹 Fn 𝐵 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐵 ) )
5	2 3 4	3bitr4g	⊢ ( 𝐴 = 𝐵 → ( 𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵 ) )