brcogw

Description: Ordered pair membership in a composition. (Contributed by Thierry Arnoux, 14-Jan-2018)

		Ref	Expression
	Assertion	brcogw	$⊢ ((A \in V \land B \in W \land X \in Z) \land (A D X \land X C B)) \to A (C \circ D) B$

Step	Hyp	Ref	Expression
1		3simpa	$⊢ (A \in V \land B \in W \land X \in Z) \to (A \in V \land B \in W)$
2		breq2	$⊢ x = X \to (A D x \leftrightarrow A D X)$
3		breq1	$⊢ x = X \to (x C B \leftrightarrow X C B)$
4	2 3	anbi12d	$⊢ x = X \to ((A D x \land x C B) \leftrightarrow (A D X \land X C B))$
5	4	spcegv	$⊢ X \in Z \to ((A D X \land X C B) \to \exists x (A D x \land x C B))$
6	5	imp	$⊢ (X \in Z \land (A D X \land X C B)) \to \exists x (A D x \land x C B)$
7	6	3ad2antl3	$⊢ ((A \in V \land B \in W \land X \in Z) \land (A D X \land X C B)) \to \exists x (A D x \land x C B)$
8		brcog	$⊢ (A \in V \land B \in W) \to (A (C \circ D) B \leftrightarrow \exists x (A D x \land x C B))$
9	8	biimpar	$⊢ ((A \in V \land B \in W) \land \exists x (A D x \land x C B)) \to A (C \circ D) B$
10	1 7 9	syl2an2r	$⊢ ((A \in V \land B \in W \land X \in Z) \land (A D X \land X C B)) \to A (C \circ D) B$

Metamath Proof Explorer