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 /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
2 1 simplbi 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )