Theorem fnrel 6640

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

Syntax hints:   → wi 4  Rel wrel 5659  Fun wfun 6525   Fn wfn 6526

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 6533  df-fn 6534

This theorem is referenced by:  fnbr  6646  fnunres1  6650  fnresdm  6657  fn0  6669  frel  6711  fcoi2  6753  f1rel  6777  f1ocnv  6830  dffn5  6937  feqmptdf  6949  fconst5  7198  fnex  7209  fnexALT  7949  tz7.48-2  8456  resfnfinfin  9349  zorn2lem4  10513  imasvscafn  17551  2oppchomf  17736  opprabs  33497  bnj66  34891  tfsconcatb0  43368  tfsconcat0i  43369  tfsconcat0b  43370  tfsconcat00  43371  fnresdmss  45192  dfafn5a  47189  oppfvallem  49081  funcoppc3  49090  uptposlem  49130