Theorem f1orel 6851

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

Syntax hints:   → wi 4  Rel wrel 5690  Fun wfun 6555  –1-1-onto→wf1o 6560

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 6563  df-fn 6564  df-f 6565  df-f1 6566  df-f1o 6568

This theorem is referenced by:  f1ococnv1  6877  isores1  7354  weisoeq2  7376  f1oexrnex  7949  ssenen  9191  f1oenfirn  9220  cantnffval2  9735  hasheqf1oi  14390  cmphaushmeo  23808  cycpmconjs  33176  poimirlem3  37630  f1ocan2fv  37734  ltrncnvnid  40129  brco2f1o  44045  brco3f1o  44046  ntrclsnvobr  44065  ntrclsiex  44066  ntrneiiex  44089  ntrneinex  44090  neicvgel1  44132  3f1oss1  47087  3f1oss2  47088