Metamath Proof Explorer


Theorem rp-fakeinunass

Description: A special case where a mixture of intersection and union appears to conform to a mixed associative law. (Contributed by RP, 26-Feb-2020)

Ref Expression
Assertion rp-fakeinunass C A A B C = A B C

Proof

Step Hyp Ref Expression
1 rp-fakeanorass x C x A x A x B x C x A x B x C
2 1 albii x x C x A x x A x B x C x A x B x C
3 dfss2 C A x x C x A
4 dfcleq A B C = A B C x x A B C x A B C
5 elun x A B C x A B x C
6 elin x A B x A x B
7 6 orbi1i x A B x C x A x B x C
8 5 7 bitri x A B C x A x B x C
9 elin x A B C x A x B C
10 elun x B C x B x C
11 10 anbi2i x A x B C x A x B x C
12 9 11 bitri x A B C x A x B x C
13 8 12 bibi12i x A B C x A B C x A x B x C x A x B x C
14 13 albii x x A B C x A B C x x A x B x C x A x B x C
15 4 14 bitri A B C = A B C x x A x B x C x A x B x C
16 2 3 15 3bitr4i C A A B C = A B C