Theorem isof1o 5931

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 5327	. 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 2508   class class class wbr 4083   -1-1-onto->wf1o 5317   ` cfv 5318   Isom wiso 5319

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 5327

This theorem is referenced by:  isocnv2  5936  isores1  5938  isoini  5942  isoini2  5943  isoselem  5944  isose  5945  isopolem  5946  isosolem  5948  smoiso  6448  isotilem  7173  supisolem  7175  supisoex  7176  supisoti  7177  ordiso2  7202  leisorel  11059  zfz1isolemiso  11061  seq3coll  11064  summodclem2a  11892  prodmodclem2a  12087