Theorem fnrel 6663

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

Assertion

Ref	Expression
fnrel	⊢ (𝐹 Fn 𝐴 → Rel 𝐹)

Proof of Theorem fnrel

Step	Hyp	Ref	Expression
1		fnfun 6661	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2		funrel 6576	. 2 ⊢ (Fun 𝐹 → Rel 𝐹)
3	1, 2	syl 18	1 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)

This proof depends on syntax axioms:   → wi 4  Rel wrel 5660  Fun wfun 6552   Fn wfn 6553

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 6560  df-fn 6561

This theorem is used by:  fnbr  6669  fnunres1  6673  fnresdm  6680  fn0  6692  frel  6737  fcoi2  6779  f1relOLD  6805  f1ocnv  6859  dffn5  6966  feqmptdf  6978  fconst5  7235  fnex  7246  fnexALT  7987  tz7.48-2  8480  zorn2lem4  10604  imasvscafn  17738  2oppchomf  17927  opprabs  34076  bnj66  35560  tfsconcatb0  44538  tfsconcat0i  44539  tfsconcat0b  44540  tfsconcat00  44541  fnresdmss  46388  dfafn5a  48435  oppfvallem  50456  funcoppc3  50468  uptposlem  50518