Theorem f1orel 6825

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 5656  Fun wfun 6531  –1-1-onto→wf1o 6536

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 6539  df-fn 6540  df-f 6541  df-f1 6542  df-f1o 6544

This theorem is used by:  f1ococnv1  6852  isores1  7340  weisoeq2  7364  f1oexrnex  7937  ssenen  9163  f1oenfirn  9188  cantnffval2  9689  hasheqf1oi  14488  cmphaushmeo  24112  cycpmconjs  33710  f1ocan2fv  38641  ltrncnvnid  41164  brco2f1o  45017  brco3f1o  45018  ntrclsnvobr  45037  ntrclsiex  45038  ntrneiiex  45061  ntrneinex  45062  neicvgel1  45104  3f1oss1  48114  3f1oss2  48115