Theorem f1orel 6785

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

Syntax hints:   → wi 4  Rel wrel 5637  Fun wfun 6494  –1-1-onto→wf1o 6499

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 6502  df-fn 6503  df-f 6504  df-f1 6505  df-f1o 6507

This theorem is referenced by:  f1ococnv1  6811  isores1  7290  weisoeq2  7312  f1oexrnex  7879  ssenen  9091  f1oenfirn  9116  cantnffval2  9616  hasheqf1oi  14286  cmphaushmeo  23756  cycpmconjs  33249  poimirlem3  37868  f1ocan2fv  37972  ltrncnvnid  40497  brco2f1o  44382  brco3f1o  44383  ntrclsnvobr  44402  ntrclsiex  44403  ntrneiiex  44426  ntrneinex  44427  neicvgel1  44469  3f1oss1  47429  3f1oss2  47430