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 A C ¬ A A

Proof

Step Hyp Ref Expression
1 cvnsym A C A C A A ¬ A A
2 1 anidms A C A A ¬ A A
3 2 pm2.01d A C ¬ A A