brcog

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

		Ref	Expression
	Assertion	brcog	$⊢ (A \in V \land B \in W) \to (A (C \circ D) B \leftrightarrow \exists x (A D x \land x C B))$

Step	Hyp	Ref	Expression
1		breq1	$⊢ y = A \to (y D x \leftrightarrow A D x)$
2		breq2	$⊢ z = B \to (x C z \leftrightarrow x C B)$
3	1 2	bi2anan9	$⊢ (y = A \land z = B) \to ((y D x \land x C z) \leftrightarrow (A D x \land x C B))$
4	3	exbidv	$⊢ (y = A \land z = B) \to (\exists x (y D x \land x C z) \leftrightarrow \exists x (A D x \land x C B))$
5		df-co	$⊢ C \circ D = \{⟨y, z⟩ \| \exists x (y D x \land x C z)\}$
6	4 5	brabga	$⊢ (A \in V \land B \in W) \to (A (C \circ D) B \leftrightarrow \exists x (A D x \land x C B))$

Metamath Proof Explorer