Theorem f1orel 6719

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

Assertion

Ref	Expression
f1orel	⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)

Proof of Theorem f1orel

Step	Hyp	Ref	Expression
1		f1ofun 6718	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹)
2		funrel 6451	. 2 ⊢ (Fun 𝐹 → Rel 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)

Syntax hints:   → wi 4  Rel wrel 5594  Fun wfun 6427  –1-1-onto→wf1o 6432

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 206  df-an 397  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-f1o 6440

This theorem is referenced by:  f1ococnv1  6745  isores1  7205  weisoeq2  7227  f1oexrnex  7774  ssenen  8938  f1oenfirn  8966  cantnffval2  9453  hasheqf1oi  14066  cmphaushmeo  22951  cycpmconjs  31423  poimirlem3  35780  f1ocan2fv  35885  ltrncnvnid  38141  brco2f1o  41642  brco3f1o  41643  ntrclsnvobr  41662  ntrclsiex  41663  ntrneiiex  41686  ntrneinex  41687  neicvgel1  41729