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 ) )