Theorem f1orel 6857

Description: A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003.)

Assertion

Ref	Expression
f1orel	⊢ (𝐹:𝐴⟶1-1onto𝐵 → Rel 𝐹)

Proof of Theorem f1orel

Step	Hyp	Ref	Expression
1		f1ofun 6856	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → Fun 𝐹)
2		funrel 6584	. 2 ⊢ (Fun 𝐹 → Rel 𝐹)
3	1, 2	syl 18	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → Rel 𝐹)

This proof depends on syntax axioms:   → wi 4  Rel wrel 5663  Fun wfun 6560  ⟶1-1ontowf1o 6565

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 6568  df-fn 6569  df-f 6570  df-f1 6571  df-f1o 6573

This theorem is used by:  f1ococnv1  6885  isores1  7373  weisoeq2  7397  f1oexrnex  7973  ssenen  9208  f1oenfirn  9233  cantnffval2  9733  hasheqf1oi  14536  cmphaushmeo  24174  cycpmconjs  33816  f1ocan2fv  38929  ltrncnvnid  41450  brco2f1o  45293  brco3f1o  45294  ntrclsnvobr  45313  ntrclsiex  45314  ntrneiiex  45337  ntrneinex  45338  neicvgel1  45380  3f1oss1  48418  3f1oss2  48419