Theorem f1orel 6813

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

Syntax hints:   → wi 4  Rel wrel 5657  Fun wfun 6519  –1-1-onto→wf1o 6524

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 210  df-an 401  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-f1o 6532

This theorem is referenced by:  f1ococnv1  6840  isores1  7322  weisoeq2  7344  f1oexrnex  7912  ssenen  9127  f1oenfirn  9152  cantnffval2  9652  hasheqf1oi  14378  cmphaushmeo  23918  cycpmconjs  33389  f1ocan2fv  38238  ltrncnvnid  40763  brco2f1o  44620  brco3f1o  44621  ntrclsnvobr  44640  ntrclsiex  44641  ntrneiiex  44664  ntrneinex  44665  neicvgel1  44707  3f1oss1  47667  3f1oss2  47668