Theorem funrel 5610

Description: A function is a relation. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
funrel

Proof of Theorem funrel

Step	Hyp	Ref	Expression
1		df-fun 5595	. 2
2	1	simplbi 460	1

Syntax hints:  ->wi 4  C_wss 3475  cid 4795  `'ccnv 5003  o.ccom 5008  Relwrel 5009  Funwfun 5587

This theorem is referenced by:  funeu  5617  nfunv  5624  funopg  5625  funssres  5633  funun  5635  fununfun  5637  fununi  5659  funcnvres2  5664  fnrel  5684  fcoi1  5764  f1orel  5824  funbrfv  5911  funbrfv2b  5917  funfv2  5941  funfvbrb  6000  fvn0ssdmfun  6022  fmptco  6064  funresdfunsn  6113  tfrlem6  7070  tfr2b  7084  pmresg  7466  fundmen  7609  resfifsupp  7877  rankwflemb  8232  gruima  9201  structcnvcnv  14643  inviso1  15160  setciso  15418  pmtrsn  16544  00lsp  17627  constr3pthlem1  24655  0eusgraiff0rgracl  24941  fimacnvinrn  27475  fmptcof2  27502  fgreu  27513  fundmpss  29196  funsseq  29199  wfrlem6  29348  frrlem5b  29392  frrlem6  29396  nofulllem3  29464  nofulllem5  29466  imageval  29580  imagesset  29603  cocnv  30216  funbrafv  32243  funbrafv2b  32244  rngciso  32790  rngcisoOLD  32802  ringciso  32841  ringcisoOLD  32865  bnj1379  33889

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