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

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 ≠ ∅