Theorem isof1o 5948

Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)

Assertion

Ref	Expression
isof1o	⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)

Proof of Theorem isof1o

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-isom 5335	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
2	1	simplbi 274	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2510   class class class wbr 4088  –1-1-onto→wf1o 5325  ‘cfv 5326   Isom wiso 5327

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 5335

This theorem is referenced by:  isocnv2  5953  isores1  5955  isoini  5959  isoini2  5960  isoselem  5961  isose  5962  isopolem  5963  isosolem  5965  smoiso  6468  isotilem  7205  supisolem  7207  supisoex  7208  supisoti  7209  ordiso2  7234  leisorel  11102  zfz1isolemiso  11104  seq3coll  11107  summodclem2a  11960  prodmodclem2a  12155