Theorem f1orel 6593

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

Syntax hints:   → wi 4  Rel wrel 5524  Fun wfun 6318  –1-1-onto→wf1o 6323

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 400  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-f1o 6331

This theorem is referenced by:  f1ococnv1  6618  isores1  7066  weisoeq2  7088  f1oexrnex  7614  ssenen  8675  cantnffval2  9142  hasheqf1oi  13708  cmphaushmeo  22405  cycpmconjs  30848  poimirlem3  35060  f1ocan2fv  35165  ltrncnvnid  37423  brco2f1o  40735  brco3f1o  40736  ntrclsnvobr  40755  ntrclsiex  40756  ntrneiiex  40779  ntrneinex  40780  neicvgel1  40822