Theorem isof1o 5878

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

Assertion

Ref	Expression
isof1o	|- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )

Proof of Theorem isof1o

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-isom 5281	. 2 |- ( 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 274	1 |- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )

Syntax hints:   -> wi 4   <-> wb 105   A.wral 2484   class class class wbr 4045   -1-1-onto->wf1o 5271   ` cfv 5272   Isom wiso 5273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-isom 5281

This theorem is referenced by:  isocnv2  5883  isores1  5885  isoini  5889  isoini2  5890  isoselem  5891  isose  5892  isopolem  5893  isosolem  5895  smoiso  6390  isotilem  7110  supisolem  7112  supisoex  7113  supisoti  7114  ordiso2  7139  leisorel  10984  zfz1isolemiso  10986  seq3coll  10989  summodclem2a  11725  prodmodclem2a  11920