Theorem f1orel 6825

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

Syntax hints:   → wi 4  Rel wrel 5668  Fun wfun 6532  –1-1-onto→wf1o 6537

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 210  df-an 401  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-f1o 6545

This theorem is referenced by:  f1ococnv1  6852  isores1  7334  weisoeq2  7356  f1oexrnex  7925  ssenen  9140  f1oenfirn  9165  cantnffval2  9665  hasheqf1oi  14389  cmphaushmeo  23938  cycpmconjs  33457  f1ocan2fv  38359  ltrncnvnid  40882  brco2f1o  44741  brco3f1o  44742  ntrclsnvobr  44761  ntrclsiex  44762  ntrneiiex  44785  ntrneinex  44786  neicvgel1  44828  3f1oss1  47795  3f1oss2  47796