| 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 6736 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
| 2 | fnrel 6670 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 Rel wrel 5690 Fn wfn 6556 ⟶wf 6557 |
| 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 6563 df-fn 6564 df-f 6565 |
| This theorem is referenced by: freld 6742 fssxp 6763 fimadmfoALT 6831 foconst 6835 fsn 7155 fnwelem 8156 mapsnd 8926 axdc3lem4 10493 imasless 17585 gimcnv 19285 gsumval3 19925 rngimcnv 20456 lmimcnv 21066 mattpostpos 22460 hmeocnv 23770 metn0 24370 rlimcnp2 27009 wlkn0 29639 cyclnumvtx 29820 tocyccntz 33164 mbfresfi 37673 rimcnv 42527 seff 44328 fresin2 45177 cncfuni 45901 fourierdlem48 46169 fourierdlem49 46170 fourierdlem113 46234 sge0cl 46396 |
| Copyright terms: Public domain | W3C validator |