Theorem isof1o 2931

Description: An isomorphism is a one-to-one onto function.

Assertion

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

Proof of Theorem isof1o

Step	Hyp	Ref	Expression
1		df-iso 2439	. 2 |- (H Isom R, S (A, B) <-> (H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))))
2	1	pm3.26bd 259	1 |- (H Isom R, S (A, B) -> H:A-1-1-onto->B)

Syntax hints:   -> wi 2   <-> wb 127  A.wral 1201   class class class wbr 2054  -1-1-onto->wf1o 2421  ` cfv 2422   Isom wiso 2423

This theorem is referenced by:  isomin 2937  isoini 2938  isofrlem 2939  isowe 2941

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-iso 2439

metamath.org