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 6045 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | fnrel 5989 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴⟶𝐵 → Rel 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Rel wrel 5119 Fn wfn 5883 ⟶wf 5884 |
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 197 df-an 386 df-fun 5890 df-fn 5891 df-f 5892 |
This theorem is referenced by: fssxp 6060 foconst 6126 fsn 6402 fnwelem 7292 mapsn 7899 axdc3lem4 9275 imasless 16200 gimcnv 17709 gsumval3 18308 lmimcnv 19067 mattpostpos 20260 hmeocnv 21565 metn0 22165 rlimcnp2 24693 wlkn0 26516 mbfresfi 33456 seff 38508 fresin2 39352 mapsnd 39388 freld 39425 cncfuni 40099 fourierdlem48 40371 fourierdlem49 40372 fourierdlem113 40436 sge0cl 40598 |
Copyright terms: Public domain | W3C validator |