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  7280  weisoeq2  7302  f1oexrnex  7869  ssenen  9079  f1oenfirn  9104  cantnffval2  9604  hasheqf1oi  14274  cmphaushmeo  23744  cycpmconjs  33238  poimirlem3  37820  f1ocan2fv  37924  ltrncnvnid  40383  brco2f1o  44269  brco3f1o  44270  ntrclsnvobr  44289  ntrclsiex  44290  ntrneiiex  44313  ntrneinex  44314  neicvgel1  44356  3f1oss1  47317  3f1oss2  47318