Theorem f1orel 5824

Description: A one-to-one onto mapping is a relation. (Contributed by NM, 13-Dec-2003.)

Assertion

Ref	Expression
f1orel

Proof of Theorem f1orel

Step	Hyp	Ref	Expression
1		f1ofun 5823	. 2
2		funrel 5610	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  Relwrel 5009  Funwfun 5587  -1-1-onto->wf1o 5592

This theorem is referenced by:  f1ococnv1  5849  isores1  6230  weisoeq2  6252  f1oexrnex  6749  ssenen  7711  cantnffval2  8135  cantnffval2OLD  8157  hasheqf1oi  12424  cmphaushmeo  20301  f1ocan2fv  30218  ltrncnvnid  35851

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 185  df-an 371  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-f1o 5600