Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Functions
freld
Next ⟩
elrnmpoid
Metamath Proof Explorer
Ascii
Unicode
Theorem
freld
Description:
A mapping is a relation.
(Contributed by
Glauco Siliprandi
, 26-Jun-2021)
Ref
Expression
Hypothesis
freld.1
⊢
φ
→
F
:
A
⟶
B
Assertion
freld
⊢
φ
→
Rel
⁡
F
Proof
Step
Hyp
Ref
Expression
1
freld.1
⊢
φ
→
F
:
A
⟶
B
2
frel
⊢
F
:
A
⟶
B
→
Rel
⁡
F
3
1
2
syl
⊢
φ
→
Rel
⁡
F