coi1in

Description: Precomposition with the identity expressed as intersection. (Contributed by BJ, 16-Aug-2026)

		Ref	Expression
	Assertion	coi1in	$⊢ A \circ I = A \cap (V \times V)$

Proof

Step	Hyp	Ref	Expression
1		19.42vv	$⊢ \exists y \exists z (x \in A \land (x = ⟨y, z⟩ \land (y \in V \land z \in V))) \leftrightarrow (x \in A \land \exists y \exists z (x = ⟨y, z⟩ \land (y \in V \land z \in V)))$
2		vex	$⊢ t \in V$
3	2	ideq	$⊢ y I t \leftrightarrow y = t$
4	3	anbi1i	$⊢ (y I t \land t A z) \leftrightarrow (y = t \land t A z)$
5		equcomi	$⊢ y = t \to t = y$
6	5	breq1d	$⊢ y = t \to (t A z \leftrightarrow y A z)$
7	6	pm5.32i	$⊢ (y = t \land t A z) \leftrightarrow (y = t \land y A z)$
8	4 7	bitri	$⊢ (y I t \land t A z) \leftrightarrow (y = t \land y A z)$
9	8	exbii	$⊢ \exists t (y I t \land t A z) \leftrightarrow \exists t (y = t \land y A z)$
10		ax6evr	$⊢ \exists t y = t$
11		19.41v	$⊢ \exists t (y = t \land y A z) \leftrightarrow (\exists t y = t \land y A z)$
12	10 11	mpbiran	$⊢ \exists t (y = t \land y A z) \leftrightarrow y A z$
13		df-br	$⊢ y A z \leftrightarrow ⟨y, z⟩ \in A$
14	9 12 13	3bitri	$⊢ \exists t (y I t \land t A z) \leftrightarrow ⟨y, z⟩ \in A$
15		eleq1	$⊢ x = ⟨y, z⟩ \to (x \in A \leftrightarrow ⟨y, z⟩ \in A)$
16	14 15	bitr4id	$⊢ x = ⟨y, z⟩ \to (\exists t (y I t \land t A z) \leftrightarrow x \in A)$
17	16	pm5.32i	$⊢ (x = ⟨y, z⟩ \land \exists t (y I t \land t A z)) \leftrightarrow (x = ⟨y, z⟩ \land x \in A)$
18	17	biancomi	$⊢ (x = ⟨y, z⟩ \land \exists t (y I t \land t A z)) \leftrightarrow (x \in A \land x = ⟨y, z⟩)$
19		vex	$⊢ y \in V$
20		vex	$⊢ z \in V$
21	19 20	pm3.2i	$⊢ (y \in V \land z \in V)$
22	21	biantru	$⊢ (x \in A \land x = ⟨y, z⟩) \leftrightarrow ((x \in A \land x = ⟨y, z⟩) \land (y \in V \land z \in V))$
23		anass	$⊢ ((x \in A \land x = ⟨y, z⟩) \land (y \in V \land z \in V)) \leftrightarrow (x \in A \land (x = ⟨y, z⟩ \land (y \in V \land z \in V)))$
24	18 22 23	3bitri	$⊢ (x = ⟨y, z⟩ \land \exists t (y I t \land t A z)) \leftrightarrow (x \in A \land (x = ⟨y, z⟩ \land (y \in V \land z \in V)))$
25	24	exbii	$⊢ \exists z (x = ⟨y, z⟩ \land \exists t (y I t \land t A z)) \leftrightarrow \exists z (x \in A \land (x = ⟨y, z⟩ \land (y \in V \land z \in V)))$
26	25	exbii	$⊢ \exists y \exists z (x = ⟨y, z⟩ \land \exists t (y I t \land t A z)) \leftrightarrow \exists y \exists z (x \in A \land (x = ⟨y, z⟩ \land (y \in V \land z \in V)))$
27		elxp	$⊢ x \in (V \times V) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (y \in V \land z \in V))$
28	27	anbi2i	$⊢ (x \in A \land x \in (V \times V)) \leftrightarrow (x \in A \land \exists y \exists z (x = ⟨y, z⟩ \land (y \in V \land z \in V)))$
29	1 26 28	3bitr4i	$⊢ \exists y \exists z (x = ⟨y, z⟩ \land \exists t (y I t \land t A z)) \leftrightarrow (x \in A \land x \in (V \times V))$
30		elco	$⊢ x \in (A \circ I) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land \exists t (y I t \land t A z))$
31		elin	$⊢ x \in (A \cap (V \times V)) \leftrightarrow (x \in A \land x \in (V \times V))$
32	29 30 31	3bitr4i	$⊢ x \in (A \circ I) \leftrightarrow x \in (A \cap (V \times V))$
33	32	eqriv	$⊢ A \circ I = A \cap (V \times V)$

Metamath Proof Explorer

Theorem coi1in

Proof