This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opelco2g

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

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

Proof

Step Hyp Ref Expression
1 brcog ⊢ A ∈ V ∧ B ∈ W → A C ∘ D B ↔ ∃ x A D x ∧ x C B
2 df-br ⊢ A C ∘ D B ↔ A B ∈ C ∘ D
3 df-br ⊢ A D x ↔ A x ∈ D
4 df-br ⊢ x C B ↔ x B ∈ C
5 3 4 anbi12i ⊢ A D x ∧ x C B ↔ A x ∈ D ∧ x B ∈ C
6 5 exbii ⊢ ∃ x A D x ∧ x C B ↔ ∃ x A x ∈ D ∧ x B ∈ C
7 1 2 6 3bitr3g ⊢ A ∈ V ∧ B ∈ W → A B ∈ C ∘ D ↔ ∃ x A x ∈ D ∧ x B ∈ C