Theorem f1orel 6805

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

Syntax hints:   → wi 4  Rel wrel 5650  Fun wfun 6511  –1-1-onto→wf1o 6516

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 209  df-an 400  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-f1o 6524

This theorem is referenced by:  f1ococnv1  6832  isores1  7314  weisoeq2  7336  f1oexrnex  7904  ssenen  9119  f1oenfirn  9144  cantnffval2  9647  hasheqf1oi  14361  cmphaushmeo  23840  cycpmconjs  33297  f1ocan2fv  38190  ltrncnvnid  40715  brco2f1o  44572  brco3f1o  44573  ntrclsnvobr  44592  ntrclsiex  44593  ntrneiiex  44616  ntrneinex  44617  neicvgel1  44659  3f1oss1  47633  3f1oss2  47634