Theorem brcog

Description: Ordered pair membership in a composition. (Contributed by NM, 24-Feb-2015)

	Ref	Expression
Assertion	brcog	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 𝐷 𝑥 ↔ 𝐴 𝐷 𝑥 ) )
2		breq2	⊢ ( 𝑧 = 𝐵 → ( 𝑥 𝐶 𝑧 ↔ 𝑥 𝐶 𝐵 ) )
3	1 2	bi2anan9	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) → ( ( 𝑦 𝐷 𝑥 ∧ 𝑥 𝐶 𝑧 ) ↔ ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) )
4	3	exbidv	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝐵 ) → ( ∃ 𝑥 ( 𝑦 𝐷 𝑥 ∧ 𝑥 𝐶 𝑧 ) ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) )
5		df-co	⊢ ( 𝐶 ∘ 𝐷 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑦 𝐷 𝑥 ∧ 𝑥 𝐶 𝑧 ) }
6	4 5	brabga	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥 ∧ 𝑥 𝐶 𝐵 ) ) )