# 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 \mathrm{dom}{R}↔\left[{A}\right]{R}\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in \mathrm{dom}{R}\to {A}\in \mathrm{V}$
2 n0 ${⊢}\left[{A}\right]{R}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left[{A}\right]{R}$
3 ecexr ${⊢}{x}\in \left[{A}\right]{R}\to {A}\in \mathrm{V}$
4 3 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left[{A}\right]{R}\to {A}\in \mathrm{V}$
5 2 4 sylbi ${⊢}\left[{A}\right]{R}\ne \varnothing \to {A}\in \mathrm{V}$
6 vex ${⊢}{x}\in \mathrm{V}$
7 elecg ${⊢}\left({x}\in \mathrm{V}\wedge {A}\in \mathrm{V}\right)\to \left({x}\in \left[{A}\right]{R}↔{A}{R}{x}\right)$
8 6 7 mpan ${⊢}{A}\in \mathrm{V}\to \left({x}\in \left[{A}\right]{R}↔{A}{R}{x}\right)$
9 8 exbidv ${⊢}{A}\in \mathrm{V}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left[{A}\right]{R}↔\exists {x}\phantom{\rule{.4em}{0ex}}{A}{R}{x}\right)$
10 2 a1i ${⊢}{A}\in \mathrm{V}\to \left(\left[{A}\right]{R}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in \left[{A}\right]{R}\right)$
11 eldmg ${⊢}{A}\in \mathrm{V}\to \left({A}\in \mathrm{dom}{R}↔\exists {x}\phantom{\rule{.4em}{0ex}}{A}{R}{x}\right)$
12 9 10 11 3bitr4rd ${⊢}{A}\in \mathrm{V}\to \left({A}\in \mathrm{dom}{R}↔\left[{A}\right]{R}\ne \varnothing \right)$
13 1 5 12 pm5.21nii ${⊢}{A}\in \mathrm{dom}{R}↔\left[{A}\right]{R}\ne \varnothing$