Theorem f1orel 6140

Description: A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003.)

Assertion

Ref	Expression
f1orel	|- ( F : A -1-1-onto-> B -> Rel F )

Proof of Theorem f1orel

Step	Hyp	Ref	Expression
1		f1ofun 6139	. 2 |- ( F : A -1-1-onto-> B -> Fun F )
2		funrel 5905	. 2 |- ( Fun F -> Rel F )
3	1, 2	syl 17	1 |- ( F : A -1-1-onto-> B -> Rel F )

Syntax hints:   -> wi 4   Rel wrel 5119   Fun wfun 5882   -1-1-onto->wf1o 5887

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 197  df-an 386  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-f1o 5895

This theorem is referenced by:  f1ococnv1  6165  isores1  6584  weisoeq2  6606  f1oexrnex  7115  ssenen  8134  cantnffval2  8592  hasheqf1oi  13140  hasheqf1oiOLD  13141  cmphaushmeo  21603  poimirlem3  33412  f1ocan2fv  33522  ltrncnvnid  35413  brco2f1o  38330  brco3f1o  38331  ntrclsnvobr  38350  ntrclsiex  38351  ntrneiiex  38374  ntrneinex  38375  neicvgel1  38417