Theorem f1orel 6830

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 5655  Fun wfun 6535  –1-1-onto→wf1o 6540

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 6543  df-fn 6544  df-f 6545  df-f1 6546  df-f1o 6548

This theorem is used by:  f1ococnv1  6857  isores1  7344  weisoeq2  7368  f1oexrnex  7941  ssenen  9175  f1oenfirn  9200  cantnffval2  9701  hasheqf1oi  14500  cmphaushmeo  24126  cycpmconjs  33765  f1ocan2fv  38768  ltrncnvnid  41291  brco2f1o  45139  brco3f1o  45140  ntrclsnvobr  45159  ntrclsiex  45160  ntrneiiex  45183  ntrneinex  45184  neicvgel1  45226  3f1oss1  48252  3f1oss2  48253