Theorem f1orel 6820

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 5660  Fun wfun 6527  –1-1-onto→wf1o 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-f1o 6540

This theorem is used by:  f1ococnv1  6847  isores1  7335  weisoeq2  7359  f1oexrnex  7924  ssenen  9149  f1oenfirn  9174  cantnffval2  9674  hasheqf1oi  14415  cmphaushmeo  24026  cycpmconjs  33596  f1ocan2fv  38477  ltrncnvnid  41000  brco2f1o  44872  brco3f1o  44873  ntrclsnvobr  44892  ntrclsiex  44893  ntrneiiex  44916  ntrneinex  44917  neicvgel1  44959  3f1oss1  47963  3f1oss2  47964