Theorem f1orel 6792

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

Syntax hints:   → wi 4  Rel wrel 5643  Fun wfun 6495  –1-1-onto→wf1o 6500

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 206  df-an 397  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-f1o 6508

This theorem is referenced by:  f1ococnv1  6818  isores1  7284  weisoeq2  7306  f1oexrnex  7869  ssenen  9102  f1oenfirn  9134  cantnffval2  9640  hasheqf1oi  14261  cmphaushmeo  23188  cycpmconjs  32075  poimirlem3  36154  f1ocan2fv  36259  ltrncnvnid  38663  brco2f1o  42426  brco3f1o  42427  ntrclsnvobr  42446  ntrclsiex  42447  ntrneiiex  42470  ntrneinex  42471  neicvgel1  42513