releldmb

Description: Membership in a domain. (Contributed by Mario Carneiro, 5-Nov-2015)

		Ref	Expression
	Assertion	releldmb	$⊢ Rel R \to (A \in dom R \leftrightarrow \exists x A R x)$

Step	Hyp	Ref	Expression
1		eldmg	$⊢ A \in dom R \to (A \in dom R \leftrightarrow \exists x A R x)$
2	1	ibi	$⊢ A \in dom R \to \exists x A R x$
3		releldm	$⊢ (Rel R \land A R x) \to A \in dom R$
4	3	ex	$⊢ Rel R \to (A R x \to A \in dom R)$
5	4	exlimdv	$⊢ Rel R \to (\exists x A R x \to A \in dom R)$
6	2 5	impbid2	$⊢ Rel R \to (A \in dom R \leftrightarrow \exists x A R x)$

Metamath Proof Explorer