Theorem f1orel 6777

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

Syntax hints:   → wi 4  Rel wrel 5629  Fun wfun 6486  –1-1-onto→wf1o 6491

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 207  df-an 396  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-f1o 6499

This theorem is referenced by:  f1ococnv1  6803  isores1  7282  weisoeq2  7304  f1oexrnex  7871  ssenen  9082  f1oenfirn  9107  cantnffval2  9607  hasheqf1oi  14304  cmphaushmeo  23775  cycpmconjs  33232  poimirlem3  37958  f1ocan2fv  38062  ltrncnvnid  40587  brco2f1o  44477  brco3f1o  44478  ntrclsnvobr  44497  ntrclsiex  44498  ntrneiiex  44521  ntrneinex  44522  neicvgel1  44564  3f1oss1  47535  3f1oss2  47536