Description: A mapping is a relation. (Contributed by Glauco Siliprandi, 26-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | freld.1 | ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) | |
Assertion | freld | ⊢ ( 𝜑 → Rel 𝐹 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | freld.1 | ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) | |
2 | frel | ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Rel 𝐹 ) | |
3 | 1 2 | syl | ⊢ ( 𝜑 → Rel 𝐹 ) |