Metamath Proof Explorer


Theorem domrefg

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

Ref Expression
Assertion domrefg ( 𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴 )

Proof

Step Hyp Ref Expression
1 enrefg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴 )
2 endom ⊢ ( 𝐴 ≈ 𝐴 → 𝐴 ≼ 𝐴 )
3 1 2 syl ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴 )