Metamath Proof Explorer


Theorem domrefg

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

Ref Expression
Assertion domrefg AVAA

Proof

Step Hyp Ref Expression
1 enrefg AVAA
2 endom AAAA
3 1 2 syl AVAA