Theorem fneq12d

Description: Equality deduction for function predicate with domain. (Contributed by NM, 26-Jun-2011)

	Ref	Expression
Hypotheses	fneq12d.1	|- ( ph -> F = G )
	fneq12d.2	|- ( ph -> A = B )
Assertion	fneq12d	|- ( ph -> ( F Fn A <-> G Fn B ) )

Proof

Step	Hyp	Ref	Expression
1		fneq12d.1	|- ( ph -> F = G )
2		fneq12d.2	|- ( ph -> A = B )
3	1	fneq1d	|- ( ph -> ( F Fn A <-> G Fn A ) )
4	2	fneq2d	|- ( ph -> ( G Fn A <-> G Fn B ) )
5	3 4	bitrd	|- ( ph -> ( F Fn A <-> G Fn B ) )