Metamath Proof Explorer


Theorem domrefg

Description: Dominance is reflexive. (Contributed by NM, 18-Jun-1998)

Ref Expression
Assertion domrefg A V A A

Proof

Step Hyp Ref Expression
1 enrefg A V A A
2 endom A A A A
3 1 2 syl A V A A