Theorem fnrel 6623

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 6621	. 2 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2		funrel 6536	. 2 ⊢ (Fun 𝐹 → Rel 𝐹)
3	1, 2	syl 17	1 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)

Syntax hints:   → wi 4  Rel wrel 5646  Fun wfun 6508   Fn wfn 6509

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 207  df-an 396  df-fun 6516  df-fn 6517

This theorem is referenced by:  fnbr  6629  fnunres1  6633  fnresdm  6640  fn0  6652  frel  6696  fcoi2  6738  f1rel  6762  f1ocnv  6815  dffn5  6922  feqmptdf  6934  fconst5  7183  fnex  7194  fnexALT  7932  tz7.48-2  8413  resfnfinfin  9295  zorn2lem4  10459  imasvscafn  17507  2oppchomf  17692  opprabs  33460  bnj66  34857  tfsconcatb0  43340  tfsconcat0i  43341  tfsconcat0b  43342  tfsconcat00  43343  fnresdmss  45169  dfafn5a  47165  oppfvallem  49128  funcoppc3  49140  uptposlem  49190