Theorem f1orel 6806

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

Syntax hints:   → wi 4  Rel wrel 5646  Fun wfun 6508  –1-1-onto→wf1o 6513

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 6516  df-fn 6517  df-f 6518  df-f1 6519  df-f1o 6521

This theorem is referenced by:  f1ococnv1  6832  isores1  7312  weisoeq2  7334  f1oexrnex  7906  ssenen  9121  f1oenfirn  9150  cantnffval2  9655  hasheqf1oi  14323  cmphaushmeo  23694  cycpmconjs  33120  poimirlem3  37624  f1ocan2fv  37728  ltrncnvnid  40128  brco2f1o  44028  brco3f1o  44029  ntrclsnvobr  44048  ntrclsiex  44049  ntrneiiex  44072  ntrneinex  44073  neicvgel1  44115  3f1oss1  47080  3f1oss2  47081