Theorem f1orel 6805

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

Syntax hints:   → wi 4  Rel wrel 5645  Fun wfun 6507  –1-1-onto→wf1o 6512

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 6515  df-fn 6516  df-f 6517  df-f1 6518  df-f1o 6520

This theorem is referenced by:  f1ococnv1  6831  isores1  7311  weisoeq2  7333  f1oexrnex  7905  ssenen  9120  f1oenfirn  9149  cantnffval2  9654  hasheqf1oi  14322  cmphaushmeo  23693  cycpmconjs  33119  poimirlem3  37612  f1ocan2fv  37716  ltrncnvnid  40116  brco2f1o  44014  brco3f1o  44015  ntrclsnvobr  44034  ntrclsiex  44035  ntrneiiex  44058  ntrneinex  44059  neicvgel1  44101  3f1oss1  47066  3f1oss2  47067