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