Metamath Proof Explorer


Theorem cvnref

Description: The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvnref ( 𝐴C → ¬ 𝐴 𝐴 )

Proof

Step Hyp Ref Expression
1 cvnsym ( ( 𝐴C𝐴C ) → ( 𝐴 𝐴 → ¬ 𝐴 𝐴 ) )
2 1 anidms ( 𝐴C → ( 𝐴 𝐴 → ¬ 𝐴 𝐴 ) )
3 2 pm2.01d ( 𝐴C → ¬ 𝐴 𝐴 )