Metamath Proof Explorer

Theorem ecdmn0

Description: A representative of a nonempty equivalence class belongs to the domain of the equivalence relation. (Contributed by NM, 15-Feb-1996) (Revised by Mario Carneiro, 9-Jul-2014)

		Ref	Expression
	Assertion	ecdmn0	$⊢ A \in dom R \leftrightarrow [A] R \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in dom R \to A \in V$
2		n0	$⊢ [A] R \neq \emptyset \leftrightarrow \exists x x \in [A] R$
3		ecexr	$⊢ x \in [A] R \to A \in V$
4	3	exlimiv	$⊢ \exists x x \in [A] R \to A \in V$
5	2 4	sylbi	$⊢ [A] R \neq \emptyset \to A \in V$
6		vex	$⊢ x \in V$
7		elecg	$⊢ (x \in V \land A \in V) \to (x \in [A] R \leftrightarrow A R x)$
8	6 7	mpan	$⊢ A \in V \to (x \in [A] R \leftrightarrow A R x)$
9	8	exbidv	$⊢ A \in V \to (\exists x x \in [A] R \leftrightarrow \exists x A R x)$
10	2	a1i	$⊢ A \in V \to ([A] R \neq \emptyset \leftrightarrow \exists x x \in [A] R)$
11		eldmg	$⊢ A \in V \to (A \in dom R \leftrightarrow \exists x A R x)$
12	9 10 11	3bitr4rd	$⊢ A \in V \to (A \in dom R \leftrightarrow [A] R \neq \emptyset)$
13	1 5 12	pm5.21nii	$⊢ A \in dom R \leftrightarrow [A] R \neq \emptyset$