Theorem f1oeq123d

Description: Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	f1eq123d.1	$$⊢\phi \to F=G$$
	f1eq123d.2	$$⊢\phi \to A=B$$
	f1eq123d.3	$$⊢\phi \to C=D$$
Assertion	f1oeq123d	$$⊢\phi \to \left(F:A\underset{1-1\; onto}{⟶}C\leftrightarrow G:B\underset{1-1\; onto}{⟶}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1eq123d.1	$$⊢\phi \to F=G$$
2		f1eq123d.2	$$⊢\phi \to A=B$$
3		f1eq123d.3	$$⊢\phi \to C=D$$
4		f1oeq1	$$⊢F=G\to \left(F:A\underset{1-1\; onto}{⟶}C\leftrightarrow G:A\underset{1-1\; onto}{⟶}C\right)$$
5	1 4	syl	$$⊢\phi \to \left(F:A\underset{1-1\; onto}{⟶}C\leftrightarrow G:A\underset{1-1\; onto}{⟶}C\right)$$
6		f1oeq2	$$⊢A=B\to \left(G:A\underset{1-1\; onto}{⟶}C\leftrightarrow G:B\underset{1-1\; onto}{⟶}C\right)$$
7	2 6	syl	$$⊢\phi \to \left(G:A\underset{1-1\; onto}{⟶}C\leftrightarrow G:B\underset{1-1\; onto}{⟶}C\right)$$
8		f1oeq3	$$⊢C=D\to \left(G:B\underset{1-1\; onto}{⟶}C\leftrightarrow G:B\underset{1-1\; onto}{⟶}D\right)$$
9	3 8	syl	$$⊢\phi \to \left(G:B\underset{1-1\; onto}{⟶}C\leftrightarrow G:B\underset{1-1\; onto}{⟶}D\right)$$
10	5 7 9	3bitrd	$$⊢\phi \to \left(F:A\underset{1-1\; onto}{⟶}C\leftrightarrow G:B\underset{1-1\; onto}{⟶}D\right)$$