Metamath Proof Explorer


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 A B H : A 1-1 onto B

Proof

Step Hyp Ref Expression
1 df-isom H Isom R , S A B H : A 1-1 onto B x A y A x R y H x S H y
2 1 simplbi H Isom R , S A B H : A 1-1 onto B