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 e. CH -> -. A

Proof

Step Hyp Ref Expression
1 cvnsym 
 |-  ( ( A e. CH /\ A e. CH ) -> ( A  -. A
2 1 anidms 
 |-  ( A e. CH -> ( A  -. A
3 2 pm2.01d 
 |-  ( A e. CH -> -. A