Metamath Proof Explorer

Theorem imaco

Description: Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006)

		Ref	Expression
	Assertion	imaco	$⊢ (A \circ B) [C] = A [B [C]]$

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists y \in B [C] y A x \leftrightarrow \exists y (y \in B [C] \land y A x)$
2		vex	$⊢ x \in V$
3	2	elima	$⊢ x \in A [B [C]] \leftrightarrow \exists y \in B [C] y A x$
4		rexcom4	$⊢ \exists z \in C \exists y (z B y \land y A x) \leftrightarrow \exists y \exists z \in C (z B y \land y A x)$
5		r19.41v	$⊢ \exists z \in C (z B y \land y A x) \leftrightarrow (\exists z \in C z B y \land y A x)$
6	5	exbii	$⊢ \exists y \exists z \in C (z B y \land y A x) \leftrightarrow \exists y (\exists z \in C z B y \land y A x)$
7	4 6	bitri	$⊢ \exists z \in C \exists y (z B y \land y A x) \leftrightarrow \exists y (\exists z \in C z B y \land y A x)$
8	2	elima	$⊢ x \in (A \circ B) [C] \leftrightarrow \exists z \in C z (A \circ B) x$
9		vex	$⊢ z \in V$
10	9 2	brco	$⊢ z (A \circ B) x \leftrightarrow \exists y (z B y \land y A x)$
11	10	rexbii	$⊢ \exists z \in C z (A \circ B) x \leftrightarrow \exists z \in C \exists y (z B y \land y A x)$
12	8 11	bitri	$⊢ x \in (A \circ B) [C] \leftrightarrow \exists z \in C \exists y (z B y \land y A x)$
13		vex	$⊢ y \in V$
14	13	elima	$⊢ y \in B [C] \leftrightarrow \exists z \in C z B y$
15	14	anbi1i	$⊢ (y \in B [C] \land y A x) \leftrightarrow (\exists z \in C z B y \land y A x)$
16	15	exbii	$⊢ \exists y (y \in B [C] \land y A x) \leftrightarrow \exists y (\exists z \in C z B y \land y A x)$
17	7 12 16	3bitr4i	$⊢ x \in (A \circ B) [C] \leftrightarrow \exists y (y \in B [C] \land y A x)$
18	1 3 17	3bitr4ri	$⊢ x \in (A \circ B) [C] \leftrightarrow x \in A [B [C]]$
19	18	eqriv	$⊢ (A \circ B) [C] = A [B [C]]$