Theorem foeq123d

Description: Equality deduction for 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	foeq123d	$$⊢\phi \to \left(F:A\underset{onto}{⟶}C\leftrightarrow G:B\underset{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		foeq1	$$⊢F=G\to \left(F:A\underset{onto}{⟶}C\leftrightarrow G:A\underset{onto}{⟶}C\right)$$
5	1 4	syl	$$⊢\phi \to \left(F:A\underset{onto}{⟶}C\leftrightarrow G:A\underset{onto}{⟶}C\right)$$
6		foeq2	$$⊢A=B\to \left(G:A\underset{onto}{⟶}C\leftrightarrow G:B\underset{onto}{⟶}C\right)$$
7	2 6	syl	$$⊢\phi \to \left(G:A\underset{onto}{⟶}C\leftrightarrow G:B\underset{onto}{⟶}C\right)$$
8		foeq3	$$⊢C=D\to \left(G:B\underset{onto}{⟶}C\leftrightarrow G:B\underset{onto}{⟶}D\right)$$
9	3 8	syl	$$⊢\phi \to \left(G:B\underset{onto}{⟶}C\leftrightarrow G:B\underset{onto}{⟶}D\right)$$
10	5 7 9	3bitrd	$$⊢\phi \to \left(F:A\underset{onto}{⟶}C\leftrightarrow G:B\underset{onto}{⟶}D\right)$$