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	⊢ ( I ∘ 𝐴 ) = ( 𝐴 ↾ V )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2	1	ideq	⊢ ( 𝑧 I 𝑦 ↔ 𝑧 = 𝑦 )
3	2	anbi2i	⊢ ( ( 𝑥 𝐴 𝑧 ∧ 𝑧 I 𝑦 ) ↔ ( 𝑥 𝐴 𝑧 ∧ 𝑧 = 𝑦 ) )
4		ancom	⊢ ( ( 𝑥 𝐴 𝑧 ∧ 𝑧 = 𝑦 ) ↔ ( 𝑧 = 𝑦 ∧ 𝑥 𝐴 𝑧 ) )
5	3 4	bitri	⊢ ( ( 𝑥 𝐴 𝑧 ∧ 𝑧 I 𝑦 ) ↔ ( 𝑧 = 𝑦 ∧ 𝑥 𝐴 𝑧 ) )
6	5	exbii	⊢ ( ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 I 𝑦 ) ↔ ∃ 𝑧 ( 𝑧 = 𝑦 ∧ 𝑥 𝐴 𝑧 ) )
7		breq2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 𝐴 𝑧 ↔ 𝑥 𝐴 𝑦 ) )
8	7	equsexvw	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑦 ∧ 𝑥 𝐴 𝑧 ) ↔ 𝑥 𝐴 𝑦 )
9	6 8	bitri	⊢ ( ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 I 𝑦 ) ↔ 𝑥 𝐴 𝑦 )
10	9	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 I 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐴 𝑦 }
11		df-co	⊢ ( I ∘ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 I 𝑦 ) }
12		relpart	⊢ ( 𝐴 ↾ V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐴 𝑦 }
13	10 11 12	3eqtr4i	⊢ ( I ∘ 𝐴 ) = ( 𝐴 ↾ V )