Metamath Proof Explorer

Theorem fneq2

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

Ref Expression
Assertion fneq2 ⊢ A = B → F Fn A ↔ F Fn B

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ A = B → dom ⁡ F = A ↔ dom ⁡ F = B
2 1 anbi2d ⊢ A = B → Fun ⁡ F ∧ dom ⁡ F = A ↔ Fun ⁡ F ∧ dom ⁡ F = B
3 df-fn ⊢ F Fn A ↔ Fun ⁡ F ∧ dom ⁡ F = A
4 df-fn ⊢ F Fn B ↔ Fun ⁡ F ∧ dom ⁡ F = B
5 2 3 4 3bitr4g ⊢ A = B → F Fn A ↔ F Fn B