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 )