Theorem isof1o 6221

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

Assertion

Ref	Expression
isof1o

Proof of Theorem isof1o

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

Step	Hyp	Ref	Expression
1		df-isom 5602	. 2
2	1	simplbi 460	1

Syntax hints:  ->wi 4  <->wb 184  A.wral 2807   class class class wbr 4452  -1-1-onto->wf1o 5592  `cfv 5593  Isomwiso 5594

This theorem is referenced by:  isores1  6230  isomin  6233  isoini  6234  isoini2  6235  isofrlem  6236  isoselem  6237  isofr  6238  isose  6239  isofr2  6240  isopolem  6241  isosolem  6243  weniso  6250  weisoeq  6251  weisoeq2  6252  wemoiso  6785  wemoiso2  6786  smoiso  7052  smoiso2  7059  supisolem  7952  supisoex  7953  supiso  7954  ordiso2  7961  ordtypelem10  7973  oiexg  7981  oien  7984  oismo  7986  cantnfle  8111  cantnflt2  8113  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1d  8128  cantnflem1  8129  cantnffval2  8135  cantnfleOLD  8141  cantnflt2OLD  8143  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1dOLD  8151  cantnflem1OLD  8152  cantnffval2OLD  8157  cantnff1o  8158  wemapwe  8160  wemapweOLD  8161  cnfcom3lem  8168  cnfcom3lemOLD  8176  infxpenlem  8412  iunfictbso  8516  dfac12lem2  8545  cofsmo  8670  isf34lem3  8776  isf34lem5  8779  hsmexlem1  8827  fpwwe2lem6  9034  fpwwe2lem7  9035  fpwwe2lem9  9037  pwfseqlem5  9062  fz1isolem  12510  seqcoll  12512  seqcoll2  12513  isercolllem2  13488  isercoll  13490  summolem2a  13537  prodmolem2a  13741  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3  16911  ordthmeolem  20302  dvne0f1  22413  dvcvx  22421  isoun  27520  erdsze2lem1  28647  fourierdlem20  31909  fourierdlem50  31939  fourierdlem51  31940  fourierdlem52  31941  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem76  31965  fourierdlem102  31991  fourierdlem114  32003

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-isom 5602