Theorem f1orel 6771

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 6770	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹)
2		funrel 6503	. 2 ⊢ (Fun 𝐹 → Rel 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Rel 𝐹)

Syntax hints:   → wi 4  Rel wrel 5628  Fun wfun 6480  –1-1-onto→wf1o 6485

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 207  df-an 396  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-f1o 6493

This theorem is referenced by:  f1ococnv1  6797  isores1  7275  weisoeq2  7297  f1oexrnex  7867  ssenen  9075  f1oenfirn  9104  cantnffval2  9610  hasheqf1oi  14276  cmphaushmeo  23703  cycpmconjs  33111  poimirlem3  37602  f1ocan2fv  37706  ltrncnvnid  40106  brco2f1o  44005  brco3f1o  44006  ntrclsnvobr  44025  ntrclsiex  44026  ntrneiiex  44049  ntrneinex  44050  neicvgel1  44092  3f1oss1  47060  3f1oss2  47061