Theorem coi1res

Description: Precomposing with the identity is the same as taking the relation part of a class. (Contributed by BJ, 16-Aug-2026)

	Ref	Expression
Assertion	coi1res	⊢ ( 𝐴 ∘ I ) = ( 𝐴 ↾ V )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑧 ∈ V
2	1	ideq	⊢ ( 𝑥 I 𝑧 ↔ 𝑥 = 𝑧 )
3		equcom	⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
4	2 3	bitri	⊢ ( 𝑥 I 𝑧 ↔ 𝑧 = 𝑥 )
5	4	anbi1i	⊢ ( ( 𝑥 I 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( 𝑧 = 𝑥 ∧ 𝑧 𝐴 𝑦 ) )
6	5	exbii	⊢ ( ∃ 𝑧 ( 𝑥 I 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 𝐴 𝑦 ) )
7		breq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝐴 𝑦 ↔ 𝑥 𝐴 𝑦 ) )
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 )