Metamath Proof Explorer


Theorem cvbr2

Description: Binary relation expressing B covers A . Definition of covers in Kalmbach p. 15. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvbr2 A C B C A B A B x C A x x B x = B

Proof

Step Hyp Ref Expression
1 cvbr A C B C A B A B ¬ x C A x x B
2 iman A x x B x = B ¬ A x x B ¬ x = B
3 anass A x x B ¬ x = B A x x B ¬ x = B
4 dfpss2 x B x B ¬ x = B
5 4 anbi2i A x x B A x x B ¬ x = B
6 3 5 bitr4i A x x B ¬ x = B A x x B
7 2 6 xchbinx A x x B x = B ¬ A x x B
8 7 ralbii x C A x x B x = B x C ¬ A x x B
9 ralnex x C ¬ A x x B ¬ x C A x x B
10 8 9 bitri x C A x x B x = B ¬ x C A x x B
11 10 anbi2i A B x C A x x B x = B A B ¬ x C A x x B
12 1 11 bitr4di A C B C A B A B x C A x x B x = B