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

This theorem is referenced by:  f1ococnv1  6803  isores1  7285  weisoeq2  7307  f1oexrnex  7874  ssenen  9086  f1oenfirn  9111  cantnffval2  9614  hasheqf1oi  14311  cmphaushmeo  23790  cycpmconjs  33244  poimirlem3  37997  f1ocan2fv  38101  ltrncnvnid  40626  brco2f1o  44483  brco3f1o  44484  ntrclsnvobr  44503  ntrclsiex  44504  ntrneiiex  44527  ntrneinex  44528  neicvgel1  44570  3f1oss1  47545  3f1oss2  47546