Theorem f1orel 6813

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

Syntax hints:   → wi 4  Rel wrel 5656  Fun wfun 6519  –1-1-onto→wf1o 6524

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 210  df-an 401  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-f1o 6532

This theorem is referenced by:  f1ococnv1  6840  isores1  7322  weisoeq2  7344  f1oexrnex  7912  ssenen  9127  f1oenfirn  9152  cantnffval2  9652  hasheqf1oi  14375  cmphaushmeo  23914  cycpmconjs  33384  f1ocan2fv  38233  ltrncnvnid  40758  brco2f1o  44615  brco3f1o  44616  ntrclsnvobr  44635  ntrclsiex  44636  ntrneiiex  44659  ntrneinex  44660  neicvgel1  44702  3f1oss1  47668  3f1oss2  47669