Theorem f1orel 6703

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

Syntax hints:   → wi 4  Rel wrel 5585  Fun wfun 6412  –1-1-onto→wf1o 6417

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 206  df-an 396  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-f1o 6425

This theorem is referenced by:  f1ococnv1  6728  isores1  7185  weisoeq2  7207  f1oexrnex  7748  ssenen  8887  f1oenfirn  8927  cantnffval2  9383  hasheqf1oi  13994  cmphaushmeo  22859  cycpmconjs  31325  poimirlem3  35707  f1ocan2fv  35812  ltrncnvnid  38068  brco2f1o  41531  brco3f1o  41532  ntrclsnvobr  41551  ntrclsiex  41552  ntrneiiex  41575  ntrneinex  41576  neicvgel1  41618