Theorem coi2res

Description: Postcomposing with the identity is the same as taking the relation part of a class. See also coi1res and coires2 . (Contributed by BJ, 8-Nov-2026)

	Ref	Expression
Assertion	coi2res	$$⊢\mathrm{I}\circ A={A\upharpoonright }_{\mathrm{V}}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2	1	ideq	$$⊢z\mathrm{I}y\leftrightarrow z=y$$
3	2	anbi2i	$$⊢\left(xAz\wedge z\mathrm{I}y\right)\leftrightarrow \left(xAz\wedge z=y\right)$$
4		ancom	$$⊢\left(xAz\wedge z=y\right)\leftrightarrow \left(z=y\wedge xAz\right)$$
5	3 4	bitri	$$⊢\left(xAz\wedge z\mathrm{I}y\right)\leftrightarrow \left(z=y\wedge xAz\right)$$
6	5	exbii	$$⊢\exists z\left(xAz\wedge z\mathrm{I}y\right)\leftrightarrow \exists z\left(z=y\wedge xAz\right)$$
7		breq2	$$⊢z=y\to \left(xAz\leftrightarrow xAy\right)$$
8	7	equsexvw	$$⊢\exists z\left(z=y\wedge xAz\right)\leftrightarrow xAy$$
9	6 8	bitri	$$⊢\exists z\left(xAz\wedge z\mathrm{I}y\right)\leftrightarrow xAy$$
10	9	opabbii	$$⊢\left\{⟨x,y⟩|\exists z\left(xAz\wedge z\mathrm{I}y\right)\right\}=\left\{⟨x,y⟩|xAy\right\}$$
11		df-co	$$⊢\mathrm{I}\circ A=\left\{⟨x,y⟩|\exists z\left(xAz\wedge z\mathrm{I}y\right)\right\}$$
12		relpart	$$⊢{A\upharpoonright }_{\mathrm{V}}=\left\{⟨x,y⟩|xAy\right\}$$
13	10 11 12	3eqtr4i	$$⊢\mathrm{I}\circ A={A\upharpoonright }_{\mathrm{V}}$$