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 5624  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  7274  weisoeq2  7296  f1oexrnex  7863  ssenen  9071  f1oenfirn  9096  cantnffval2  9592  hasheqf1oi  14260  cmphaushmeo  23716  cycpmconjs  33132  poimirlem3  37684  f1ocan2fv  37788  ltrncnvnid  40247  brco2f1o  44150  brco3f1o  44151  ntrclsnvobr  44170  ntrclsiex  44171  ntrneiiex  44194  ntrneinex  44195  neicvgel1  44237  3f1oss1  47200  3f1oss2  47201