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	|- ( A C_ C <-> ( ( A u. B ) i^i C ) = ( A u. ( B i^i C ) ) )

Proof

Step	Hyp	Ref	Expression
1		rp-fakeinunass	|- ( A C_ C <-> ( ( C i^i B ) u. A ) = ( C i^i ( B u. A ) ) )
2		eqcom	|- ( ( ( C i^i B ) u. A ) = ( C i^i ( B u. A ) ) <-> ( C i^i ( B u. A ) ) = ( ( C i^i B ) u. A ) )
3		incom	|- ( C i^i ( B u. A ) ) = ( ( B u. A ) i^i C )
4		uncom	|- ( B u. A ) = ( A u. B )
5	4	ineq1i	|- ( ( B u. A ) i^i C ) = ( ( A u. B ) i^i C )
6	3 5	eqtri	|- ( C i^i ( B u. A ) ) = ( ( A u. B ) i^i C )
7		uncom	|- ( ( C i^i B ) u. A ) = ( A u. ( C i^i B ) )
8		incom	|- ( C i^i B ) = ( B i^i C )
9	8	uneq2i	|- ( A u. ( C i^i B ) ) = ( A u. ( B i^i C ) )
10	7 9	eqtri	|- ( ( C i^i B ) u. A ) = ( A u. ( B i^i C ) )
11	6 10	eqeq12i	|- ( ( C i^i ( B u. A ) ) = ( ( C i^i B ) u. A ) <-> ( ( A u. B ) i^i C ) = ( A u. ( B i^i C ) ) )
12	1 2 11	3bitri	|- ( A C_ C <-> ( ( A u. B ) i^i C ) = ( A u. ( B i^i C ) ) )