fneq2

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

		Ref	Expression
	Assertion	fneq2	$⊢ A = B \to (F Fn A \leftrightarrow F Fn B)$

Step	Hyp	Ref	Expression
1		eqeq2	$⊢ A = B \to (dom F = A \leftrightarrow dom F = B)$
2	1	anbi2d	$⊢ A = B \to ((Fun F \land dom F = A) \leftrightarrow (Fun F \land dom F = B))$
3		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
4		df-fn	$⊢ F Fn B \leftrightarrow (Fun F \land dom F = B)$
5	2 3 4	3bitr4g	$⊢ A = B \to (F Fn A \leftrightarrow F Fn B)$

Metamath Proof Explorer