Metamath Proof Explorer

Theorem brcog

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

Ref Expression
Assertion brcog ⊢ A ∈ V ∧ B ∈ W → A C ∘ D B ↔ ∃ x A D x ∧ x C B

Proof

Step Hyp Ref Expression
1 breq1 ⊢ y = A → y D x ↔ A D x
2 breq2 ⊢ z = B → x C z ↔ x C B
3 1 2 bi2anan9 ⊢ y = A ∧ z = B → y D x ∧ x C z ↔ A D x ∧ x C B
4 3 exbidv ⊢ y = A ∧ z = B → ∃ x y D x ∧ x C z ↔ ∃ x A D x ∧ x C B
5 df-co ⊢ C ∘ D = y z | ∃ x y D x ∧ x C z
6 4 5 brabga ⊢ A ∈ V ∧ B ∈ W → A C ∘ D B ↔ ∃ x A D x ∧ x C B