Theorem f1orel 6620

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

Syntax hints:   → wi 4  Rel wrel 5562  Fun wfun 6351  –1-1-onto→wf1o 6356

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 209  df-an 399  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-f1o 6364

This theorem is referenced by:  f1ococnv1  6645  isores1  7089  weisoeq2  7111  f1oexrnex  7634  ssenen  8693  cantnffval2  9160  hasheqf1oi  13715  cmphaushmeo  22410  cycpmconjs  30800  poimirlem3  34897  f1ocan2fv  35004  ltrncnvnid  37265  brco2f1o  40389  brco3f1o  40390  ntrclsnvobr  40409  ntrclsiex  40410  ntrneiiex  40433  ntrneinex  40434  neicvgel1  40476