elco

		Ref	Expression
	Assertion	elco	$⊢ A \in (C \circ B) \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land \exists z (x B z \land z C y))$

Step	Hyp	Ref	Expression
1		df-co	$⊢ C \circ B = \{⟨x, y⟩ \| \exists z (x B z \land z C y)\}$
2	1	eleq2i	$⊢ A \in (C \circ B) \leftrightarrow A \in \{⟨x, y⟩ \| \exists z (x B z \land z C y)\}$
3		elopab	$⊢ A \in \{⟨x, y⟩ \| \exists z (x B z \land z C y)\} \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land \exists z (x B z \land z C y))$
4	2 3	bitri	$⊢ A \in (C \circ B) \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land \exists z (x B z \land z C y))$

Metamath Proof Explorer