Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fneq1i.1 | ⊢ 𝐹 = 𝐺 | |
Assertion | fneq1i | ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq1i.1 | ⊢ 𝐹 = 𝐺 | |
2 | fneq1 | ⊢ ( 𝐹 = 𝐺 → ( 𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴 ) ) | |
3 | 1 2 | ax-mp | ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴 ) |