Metamath Proof Explorer

Theorem fneq1

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

Ref Expression
Assertion fneq1 ⊢ F = G → F Fn A ↔ G Fn A

Proof

Step Hyp Ref Expression
1 funeq ⊢ F = G → Fun ⁡ F ↔ Fun ⁡ G
2 dmeq ⊢ F = G → dom ⁡ F = dom ⁡ G
3 2 eqeq1d ⊢ F = G → dom ⁡ F = A ↔ dom ⁡ G = A
4 1 3 anbi12d ⊢ F = G → Fun ⁡ F ∧ dom ⁡ F = A ↔ Fun ⁡ G ∧ dom ⁡ G = A
5 df-fn ⊢ F Fn A ↔ Fun ⁡ F ∧ dom ⁡ F = A
6 df-fn ⊢ G Fn A ↔ Fun ⁡ G ∧ dom ⁡ G = A
7 4 5 6 3bitr4g ⊢ F = G → F Fn A ↔ G Fn A