![]() |
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 6344 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | fnrel 6287 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Rel wrel 5412 Fn wfn 6183 ⟶wf 6184 |
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 199 df-an 388 df-fun 6190 df-fn 6191 df-f 6192 |
This theorem is referenced by: fssxp 6363 fimadmfoALT 6430 foconst 6432 fsn 6720 fnwelem 7630 mapsnd 8248 axdc3lem4 9673 imasless 16669 gimcnv 18178 gsumval3 18781 lmimcnv 19561 mattpostpos 20767 hmeocnv 22074 metn0 22673 rlimcnp2 25246 wlkn0 27105 mbfresfi 34376 seff 40054 fresin2 40850 freld 40917 cncfuni 41597 fourierdlem48 41868 fourierdlem49 41869 fourierdlem113 41933 sge0cl 42092 |
Copyright terms: Public domain | W3C validator |