Theorem f1orel 6827

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

This proof depends on syntax axioms:   → wi 4  Rel wrel 5668  Fun wfun 6534  –1-1-onto→wf1o 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-f1o 6547

This theorem is used by:  f1ococnv1  6854  isores1  7338  weisoeq2  7362  f1oexrnex  7926  ssenen  9142  f1oenfirn  9167  cantnffval2  9667  hasheqf1oi  14400  cmphaushmeo  23986  cycpmconjs  33499  f1ocan2fv  38411  ltrncnvnid  40934  brco2f1o  44791  brco3f1o  44792  ntrclsnvobr  44811  ntrclsiex  44812  ntrneiiex  44835  ntrneinex  44836  neicvgel1  44878  3f1oss1  47845  3f1oss2  47846