Theorem f1orel 6865

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

Syntax hints:   → wi 4  Rel wrel 5705  Fun wfun 6567  –1-1-onto→wf1o 6572

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 6575  df-fn 6576  df-f 6577  df-f1 6578  df-f1o 6580

This theorem is referenced by:  f1ococnv1  6891  isores1  7370  weisoeq2  7392  f1oexrnex  7967  ssenen  9217  f1oenfirn  9246  cantnffval2  9764  hasheqf1oi  14400  cmphaushmeo  23829  cycpmconjs  33149  poimirlem3  37583  f1ocan2fv  37687  ltrncnvnid  40084  brco2f1o  43994  brco3f1o  43995  ntrclsnvobr  44014  ntrclsiex  44015  ntrneiiex  44038  ntrneinex  44039  neicvgel1  44081  3f1oss1  46990  3f1oss2  46991