foeq2

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

		Ref	Expression
	Assertion	foeq2	$⊢ A = B \to (F : A \underset{onto}{⟶} C \leftrightarrow F : B \underset{onto}{⟶} C)$

Step	Hyp	Ref	Expression
1		fneq2	$⊢ A = B \to (F Fn A \leftrightarrow F Fn B)$
2	1	anbi1d	$⊢ A = B \to ((F Fn A \land ran F = C) \leftrightarrow (F Fn B \land ran F = C))$
3		df-fo	$⊢ F : A \underset{onto}{⟶} C \leftrightarrow (F Fn A \land ran F = C)$
4		df-fo	$⊢ F : B \underset{onto}{⟶} C \leftrightarrow (F Fn B \land ran F = C)$
5	2 3 4	3bitr4g	$⊢ A = B \to (F : A \underset{onto}{⟶} C \leftrightarrow F : B \underset{onto}{⟶} C)$

Metamath Proof Explorer