Theorem f1orel 6803

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

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

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 6513  df-fn 6514  df-f 6515  df-f1 6516  df-f1o 6518

This theorem is referenced by:  f1ococnv1  6829  isores1  7309  weisoeq2  7331  f1oexrnex  7903  ssenen  9115  f1oenfirn  9144  cantnffval2  9648  hasheqf1oi  14316  cmphaushmeo  23687  cycpmconjs  33113  poimirlem3  37617  f1ocan2fv  37721  ltrncnvnid  40121  brco2f1o  44021  brco3f1o  44022  ntrclsnvobr  44041  ntrclsiex  44042  ntrneiiex  44065  ntrneinex  44066  neicvgel1  44108  3f1oss1  47076  3f1oss2  47077