Metamath Proof Explorer


Theorem fneq1i

Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Hypothesis fneq1i.1 F = G
Assertion fneq1i F Fn A G Fn A

Proof

Step Hyp Ref Expression
1 fneq1i.1 F = G
2 fneq1 F = G F Fn A G Fn A
3 1 2 ax-mp F Fn A G Fn A