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 \in V \land B \in W) \to (⟨A, B⟩ \in (C \circ D) \leftrightarrow \exists x (⟨A, x⟩ \in D \land ⟨x, B⟩ \in C))$

Step	Hyp	Ref	Expression
1		brcog	$⊢ (A \in V \land B \in W) \to (A (C \circ D) B \leftrightarrow \exists x (A D x \land x C B))$
2		df-br	$⊢ A (C \circ D) B \leftrightarrow ⟨A, B⟩ \in (C \circ D)$
3		df-br	$⊢ A D x \leftrightarrow ⟨A, x⟩ \in D$
4		df-br	$⊢ x C B \leftrightarrow ⟨x, B⟩ \in C$
5	3 4	anbi12i	$⊢ (A D x \land x C B) \leftrightarrow (⟨A, x⟩ \in D \land ⟨x, B⟩ \in C)$
6	5	exbii	$⊢ \exists x (A D x \land x C B) \leftrightarrow \exists x (⟨A, x⟩ \in D \land ⟨x, B⟩ \in C)$
7	1 2 6	3bitr3g	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ \in (C \circ D) \leftrightarrow \exists x (⟨A, x⟩ \in D \land ⟨x, B⟩ \in C))$

Metamath Proof Explorer