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 ∧ ∀x ∈ A ∀y ∈ 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  ∀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