This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem f1oeq1d

Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypothesis	f1oeq1d.1	$⊢ φ \to F = G$
	Assertion	f1oeq1d	$⊢ φ \to (F : A \underset{1-1 onto}{⟶} B \leftrightarrow G : A \underset{1-1 onto}{⟶} B)$

Step	Hyp	Ref	Expression
1		f1oeq1d.1	$⊢ φ \to F = G$
2		f1oeq1	$⊢ F = G \to (F : A \underset{1-1 onto}{⟶} B \leftrightarrow G : A \underset{1-1 onto}{⟶} B)$
3	1 2	syl	$⊢ φ \to (F : A \underset{1-1 onto}{⟶} B \leftrightarrow G : A \underset{1-1 onto}{⟶} B)$