Theorem isof1o 5876

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 5280	. 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 4044   -1-1-onto->wf1o 5270   ` cfv 5271   Isom wiso 5272

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 5280

This theorem is referenced by:  isocnv2  5881  isores1  5883  isoini  5887  isoini2  5888  isoselem  5889  isose  5890  isopolem  5891  isosolem  5893  smoiso  6388  isotilem  7108  supisolem  7110  supisoex  7111  supisoti  7112  ordiso2  7137  leisorel  10982  zfz1isolemiso  10984  seq3coll  10987  summodclem2a  11692  prodmodclem2a  11887