fneq1

Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994)

		Ref	Expression
	Assertion	fneq1	$⊢ F = G \to (F Fn A \leftrightarrow G Fn A)$

Step	Hyp	Ref	Expression
1		funeq	$⊢ F = G \to (Fun F \leftrightarrow Fun G)$
2		dmeq	$⊢ F = G \to dom F = dom G$
3	2	eqeq1d	$⊢ F = G \to (dom F = A \leftrightarrow dom G = A)$
4	1 3	anbi12d	$⊢ F = G \to ((Fun F \land dom F = A) \leftrightarrow (Fun G \land dom G = A))$
5		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
6		df-fn	$⊢ G Fn A \leftrightarrow (Fun G \land dom G = A)$
7	4 5 6	3bitr4g	$⊢ F = G \to (F Fn A \leftrightarrow G Fn A)$

Metamath Proof Explorer