Theorem isof1o 5808

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 5226	. 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 2455   class class class wbr 4004   -1-1-onto->wf1o 5216   ` cfv 5217   Isom wiso 5218

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 5226

This theorem is referenced by:  isocnv2  5813  isores1  5815  isoini  5819  isoini2  5820  isoselem  5821  isose  5822  isopolem  5823  isosolem  5825  smoiso  6303  isotilem  7005  supisolem  7007  supisoex  7008  supisoti  7009  ordiso2  7034  leisorel  10817  zfz1isolemiso  10819  seq3coll  10822  summodclem2a  11389  prodmodclem2a  11584