Theorem f1orel 6826

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

Syntax hints:   → wi 4  Rel wrel 5664  Fun wfun 6530  –1-1-onto→wf1o 6535

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 6538  df-fn 6539  df-f 6540  df-f1 6541  df-f1o 6543

This theorem is referenced by:  f1ococnv1  6852  isores1  7332  weisoeq2  7354  f1oexrnex  7928  ssenen  9170  f1oenfirn  9199  cantnffval2  9714  hasheqf1oi  14374  cmphaushmeo  23743  cycpmconjs  33172  poimirlem3  37652  f1ocan2fv  37756  ltrncnvnid  40151  brco2f1o  44023  brco3f1o  44024  ntrclsnvobr  44043  ntrclsiex  44044  ntrneiiex  44067  ntrneinex  44068  neicvgel1  44110  3f1oss1  47071  3f1oss2  47072