![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > frel | Structured version Visualization version GIF version |
Description: A mapping is a relation. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
frel | ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 6723 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | fnrel 6657 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Rel wrel 5683 Fn wfn 6544 ⟶wf 6545 |
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 206 df-an 395 df-fun 6551 df-fn 6552 df-f 6553 |
This theorem is referenced by: freld 6729 fssxp 6751 fimadmfoALT 6821 foconst 6825 fsn 7144 fnwelem 8136 mapsnd 8905 axdc3lem4 10478 imasless 17525 gimcnv 19230 gsumval3 19874 rngimcnv 20407 lmimcnv 20964 mattpostpos 22400 hmeocnv 23710 metn0 24310 rlimcnp2 26943 wlkn0 29507 tocyccntz 32957 mbfresfi 37270 rimcnv 41892 seff 43888 fresin2 44684 cncfuni 45412 fourierdlem48 45680 fourierdlem49 45681 fourierdlem113 45745 sge0cl 45907 |
Copyright terms: Public domain | W3C validator |