Metamath Proof Explorer

Theorem opelco

Description: Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996) (Revised by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses opelco.1 ⊢ A ∈ V
opelco.2 ⊢ B ∈ V
Assertion opelco ⊢ A B ∈ C ∘ D ↔ ∃ x A D x ∧ x C B

Proof

Step Hyp Ref Expression
1 opelco.1 ⊢ A ∈ V
2 opelco.2 ⊢ B ∈ V
3 df-br ⊢ A C ∘ D B ↔ A B ∈ C ∘ D
4 1 2 brco ⊢ A C ∘ D B ↔ ∃ x A D x ∧ x C B
5 3 4 bitr3i ⊢ A B ∈ C ∘ D ↔ ∃ x A D x ∧ x C B