Metamath Proof Explorer


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 ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 ( 𝐶𝐷 ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 𝐷 𝑥𝑥 𝐶 𝐵 ) ) )