Theorem f1orel 6783

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

Syntax hints:   → wi 4  Rel wrel 5636  Fun wfun 6492  –1-1-onto→wf1o 6497

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 6500  df-fn 6501  df-f 6502  df-f1 6503  df-f1o 6505

This theorem is referenced by:  f1ococnv1  6809  isores1  7289  weisoeq2  7311  f1oexrnex  7878  ssenen  9089  f1oenfirn  9114  cantnffval2  9616  hasheqf1oi  14313  cmphaushmeo  23765  cycpmconjs  33217  poimirlem3  37944  f1ocan2fv  38048  ltrncnvnid  40573  brco2f1o  44459  brco3f1o  44460  ntrclsnvobr  44479  ntrclsiex  44480  ntrneiiex  44503  ntrneinex  44504  neicvgel1  44546  3f1oss1  47523  3f1oss2  47524