feq1

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994)

		Ref	Expression
	Assertion	feq1	$⊢ F = G \to (F : A ⟶ B \leftrightarrow G : A ⟶ B)$

Step	Hyp	Ref	Expression
1		fneq1	$⊢ F = G \to (F Fn A \leftrightarrow G Fn A)$
2		rneq	$⊢ F = G \to ran F = ran G$
3	2	sseq1d	$⊢ F = G \to (ran F \subseteq B \leftrightarrow ran G \subseteq B)$
4	1 3	anbi12d	$⊢ F = G \to ((F Fn A \land ran F \subseteq B) \leftrightarrow (G Fn A \land ran G \subseteq B))$
5		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
6		df-f	$⊢ G : A ⟶ B \leftrightarrow (G Fn A \land ran G \subseteq B)$
7	4 5 6	3bitr4g	$⊢ F = G \to (F : A ⟶ B \leftrightarrow G : A ⟶ B)$

Metamath Proof Explorer