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	⊢ ( 𝐶 ⊆ 𝐴 ↔ ( ( 𝐴 ∩ 𝐵 ) ∪ 𝐶 ) = ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rp-fakeanorass	⊢ ( ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∨ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) ) ) )
2	1	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) ↔ ∀ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∨ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) ) ) )
3		df-ss	⊢ ( 𝐶 ⊆ 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 ) )
4		dfcleq	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∪ 𝐶 ) = ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∪ 𝐶 ) ↔ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) ) )
5		elun	⊢ ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∪ 𝐶 ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∨ 𝑥 ∈ 𝐶 ) )
6		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
7	6	orbi1i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∨ 𝑥 ∈ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∨ 𝑥 ∈ 𝐶 ) )
8	5 7	bitri	⊢ ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∪ 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∨ 𝑥 ∈ 𝐶 ) )
9		elin	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 ∪ 𝐶 ) ) )
10		elun	⊢ ( 𝑥 ∈ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) )
11	10	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 ∪ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) ) )
12	9 11	bitri	⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) ) )
13	8 12	bibi12i	⊢ ( ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∪ 𝐶 ) ↔ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∨ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) ) ) )
14	13	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( ( 𝐴 ∩ 𝐵 ) ∪ 𝐶 ) ↔ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) ) ↔ ∀ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∨ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) ) ) )
15	4 14	bitri	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∪ 𝐶 ) = ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) ↔ ∀ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∨ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶 ) ) ) )
16	2 3 15	3bitr4i	⊢ ( 𝐶 ⊆ 𝐴 ↔ ( ( 𝐴 ∩ 𝐵 ) ∪ 𝐶 ) = ( 𝐴 ∩ ( 𝐵 ∪ 𝐶 ) ) )