Theorem elco

Description: Membership in a composition. (Contributed by BJ, 16-Aug-2026)

	Ref	Expression
Assertion	elco	⊢ ( 𝐴 ∈ ( 𝐶 ∘ 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐶 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-co	⊢ ( 𝐶 ∘ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐶 𝑦 ) }
2	1	eleq2i	⊢ ( 𝐴 ∈ ( 𝐶 ∘ 𝐵 ) ↔ 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐶 𝑦 ) } )
3		elopab	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐶 𝑦 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐶 𝑦 ) ) )
4	2 3	bitri	⊢ ( 𝐴 ∈ ( 𝐶 ∘ 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐶 𝑦 ) ) )