Theorem f1orel 6824

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

Syntax hints:   → wi 4  Rel wrel 5667  Fun wfun 6531  –1-1-onto→wf1o 6536

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 6539  df-fn 6540  df-f 6541  df-f1 6542  df-f1o 6544

This theorem is referenced by:  f1ococnv1  6851  isores1  7333  weisoeq2  7355  f1oexrnex  7923  ssenen  9138  f1oenfirn  9163  cantnffval2  9663  hasheqf1oi  14386  cmphaushmeo  23925  cycpmconjs  33416  f1ocan2fv  38265  ltrncnvnid  40790  brco2f1o  44649  brco3f1o  44650  ntrclsnvobr  44669  ntrclsiex  44670  ntrneiiex  44693  ntrneinex  44694  neicvgel1  44736  3f1oss1  47700  3f1oss2  47701