imaco

Description: Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006) (Proof shortened by Wolf Lammen, 16-May-2025)

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

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		vex	$⊢ z \in V$
5	4 2	brco	$⊢ z (A \circ B) x \leftrightarrow \exists y (z B y \land y A x)$
6	5	rexbii	$⊢ \exists z \in C z (A \circ B) x \leftrightarrow \exists z \in C \exists y (z B y \land y A x)$
7		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)$
8		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)$
9	8	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)$
10	6 7 9	3bitri	$⊢ \exists z \in C z (A \circ B) x \leftrightarrow \exists y (\exists z \in C z B y \land y A x)$
11	2	elima	$⊢ x \in (A \circ B) [C] \leftrightarrow \exists z \in C z (A \circ B) x$
12		vex	$⊢ y \in V$
13	12	elima	$⊢ y \in B [C] \leftrightarrow \exists z \in C z B y$
14	13	anbi1i	$⊢ (y \in B [C] \land y A x) \leftrightarrow (\exists z \in C z B y \land y A x)$
15	14	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)$
16	10 11 15	3bitr4i	$⊢ x \in (A \circ B) [C] \leftrightarrow \exists y (y \in B [C] \land y A x)$
17	1 3 16	3bitr4ri	$⊢ x \in (A \circ B) [C] \leftrightarrow x \in A [B [C]]$
18	17	eqriv	$⊢ (A \circ B) [C] = A [B [C]]$

Metamath Proof Explorer