Metamath Proof Explorer

Theorem cvpss

Description: The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvpss 
|- ( ( A e. CH /\ B e. CH ) -> ( A  A C. B ) )

Proof

Step Hyp Ref Expression
1 cvbr 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) ) )
2 simpl 
 |-  ( ( A C. B /\ -. E. x e. CH ( A C. x /\ x C. B ) ) -> A C. B )
3 1 2 syl6bi 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A  A C. B ) )