Metamath Proof Explorer


Theorem inimasn

Description: The intersection of the image of singleton. (Contributed by Thierry Arnoux, 16-Dec-2017)

Ref Expression
Assertion inimasn CVABC=ACBC

Proof

Step Hyp Ref Expression
1 elin xACBCxACxBC
2 elin CxABCxACxB
3 2 a1i CVCxABCxACxB
4 elimasng CVxVxABCCxAB
5 4 elvd CVxABCCxAB
6 elimasng CVxVxACCxA
7 6 elvd CVxACCxA
8 elimasng CVxVxBCCxB
9 8 elvd CVxBCCxB
10 7 9 anbi12d CVxACxBCCxACxB
11 3 5 10 3bitr4rd CVxACxBCxABC
12 1 11 bitr2id CVxABCxACBC
13 12 eqrdv CVABC=ACBC