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

Metamath Proof Explorer

Theorem elima3

Description: Membership in an image. Theorem 34 of Suppes p. 65. (Contributed by NM, 14-Aug-1994)

		Ref	Expression
	Hypothesis	elima.1	$⊢ A \in V$
	Assertion	elima3	$⊢ A \in B [C] \leftrightarrow \exists x (x \in C \land ⟨x, A⟩ \in B)$

Step	Hyp	Ref	Expression
1		elima.1	$⊢ A \in V$
2	1	elima2	$⊢ A \in B [C] \leftrightarrow \exists x (x \in C \land x B A)$
3		df-br	$⊢ x B A \leftrightarrow ⟨x, A⟩ \in B$
4	3	anbi2i	$⊢ (x \in C \land x B A) \leftrightarrow (x \in C \land ⟨x, A⟩ \in B)$
5	4	exbii	$⊢ \exists x (x \in C \land x B A) \leftrightarrow \exists x (x \in C \land ⟨x, A⟩ \in B)$
6	2 5	bitri	$⊢ A \in B [C] \leftrightarrow \exists x (x \in C \land ⟨x, A⟩ \in B)$