Theorem f1orel 6766

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

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

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 6483  df-fn 6484  df-f 6485  df-f1 6486  df-f1o 6488

This theorem is referenced by:  f1ococnv1  6792  isores1  7268  weisoeq2  7290  f1oexrnex  7857  ssenen  9064  f1oenfirn  9089  cantnffval2  9585  hasheqf1oi  14258  cmphaushmeo  23716  cycpmconjs  33123  poimirlem3  37669  f1ocan2fv  37773  ltrncnvnid  40172  brco2f1o  44071  brco3f1o  44072  ntrclsnvobr  44091  ntrclsiex  44092  ntrneiiex  44115  ntrneinex  44116  neicvgel1  44158  3f1oss1  47112  3f1oss2  47113