Theorem isof1o

Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004)

	Ref	Expression
Assertion	isof1o	$$⊢H{Isom}_{R,S}\left(A,B\right)\to H:A\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		df-isom	$$⊢H{Isom}_{R,S}\left(A,B\right)\leftrightarrow \left(H:A\underset{1-1\; onto}{⟶}B\wedge \forall x\in A\forall y\in A\left(xRy\leftrightarrow H\left(x\right)SH\left(y\right)\right)\right)$$
2	1	simplbi	$$⊢H{Isom}_{R,S}\left(A,B\right)\to H:A\underset{1-1\; onto}{⟶}B$$