This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem domrefg

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

Ref Expression
Assertion domrefg 
|- ( A e. V -> A ~<_ A )

Proof

Step Hyp Ref Expression
1 enrefg 
 |-  ( A e. V -> A ~~ A )
2 endom 
 |-  ( A ~~ A -> A ~<_ A )
3 1 2 syl 
 |-  ( A e. V -> A ~<_ A )