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 dom R A R

Proof

Step Hyp Ref Expression
1 elex A dom R A V
2 n0 A R x x A R
3 ecexr x A R A V
4 3 exlimiv x x A R A V
5 2 4 sylbi A R A V
6 vex x V
7 elecg x V A V x A R A R x
8 6 7 mpan A V x A R A R x
9 8 exbidv A V x x A R x A R x
10 2 a1i A V A R x x A R
11 eldmg A V A dom R x A R x
12 9 10 11 3bitr4rd A V A dom R A R
13 1 5 12 pm5.21nii A dom R A R