Theorem rp-fakeuninass

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

	Ref	Expression
Assertion	rp-fakeuninass	⊢ ( 𝐴 ⊆ 𝐶 ↔ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 ) = ( 𝐴 ∪ ( 𝐵 ∩ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rp-fakeinunass	⊢ ( 𝐴 ⊆ 𝐶 ↔ ( ( 𝐶 ∩ 𝐵 ) ∪ 𝐴 ) = ( 𝐶 ∩ ( 𝐵 ∪ 𝐴 ) ) )
2		eqcom	⊢ ( ( ( 𝐶 ∩ 𝐵 ) ∪ 𝐴 ) = ( 𝐶 ∩ ( 𝐵 ∪ 𝐴 ) ) ↔ ( 𝐶 ∩ ( 𝐵 ∪ 𝐴 ) ) = ( ( 𝐶 ∩ 𝐵 ) ∪ 𝐴 ) )
3		incom	⊢ ( 𝐶 ∩ ( 𝐵 ∪ 𝐴 ) ) = ( ( 𝐵 ∪ 𝐴 ) ∩ 𝐶 )
4		uncom	⊢ ( 𝐵 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 )
5	4	ineq1i	⊢ ( ( 𝐵 ∪ 𝐴 ) ∩ 𝐶 ) = ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 )
6	3 5	eqtri	⊢ ( 𝐶 ∩ ( 𝐵 ∪ 𝐴 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 )
7		uncom	⊢ ( ( 𝐶 ∩ 𝐵 ) ∪ 𝐴 ) = ( 𝐴 ∪ ( 𝐶 ∩ 𝐵 ) )
8		incom	⊢ ( 𝐶 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐶 )
9	8	uneq2i	⊢ ( 𝐴 ∪ ( 𝐶 ∩ 𝐵 ) ) = ( 𝐴 ∪ ( 𝐵 ∩ 𝐶 ) )
10	7 9	eqtri	⊢ ( ( 𝐶 ∩ 𝐵 ) ∪ 𝐴 ) = ( 𝐴 ∪ ( 𝐵 ∩ 𝐶 ) )
11	6 10	eqeq12i	⊢ ( ( 𝐶 ∩ ( 𝐵 ∪ 𝐴 ) ) = ( ( 𝐶 ∩ 𝐵 ) ∪ 𝐴 ) ↔ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 ) = ( 𝐴 ∪ ( 𝐵 ∩ 𝐶 ) ) )
12	1 2 11	3bitri	⊢ ( 𝐴 ⊆ 𝐶 ↔ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐶 ) = ( 𝐴 ∪ ( 𝐵 ∩ 𝐶 ) ) )