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 ( 𝐴 ∈ dom 𝑅 ↔ [ 𝐴 ] 𝑅 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ dom 𝑅 → 𝐴 ∈ V )
2 n0 ⊢ ( [ 𝐴 ] 𝑅 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ [ 𝐴 ] 𝑅 )
3 ecexr ⊢ ( 𝑥 ∈ [ 𝐴 ] 𝑅 → 𝐴 ∈ V )
4 3 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ [ 𝐴 ] 𝑅 → 𝐴 ∈ V )
5 2 4 sylbi ⊢ ( [ 𝐴 ] 𝑅 ≠ ∅ → 𝐴 ∈ V )
6 vex ⊢ 𝑥 ∈ V
7 elecg ⊢ ( ( 𝑥 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
8 6 7 mpan ⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ 𝐴 𝑅 𝑥 ) )
9 8 exbidv ⊢ ( 𝐴 ∈ V → ( ∃ 𝑥 𝑥 ∈ [ 𝐴 ] 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) )
10 2 a1i ⊢ ( 𝐴 ∈ V → ( [ 𝐴 ] 𝑅 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ [ 𝐴 ] 𝑅 ) )
11 eldmg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ dom 𝑅 ↔ ∃ 𝑥 𝐴 𝑅 𝑥 ) )
12 9 10 11 3bitr4rd ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ dom 𝑅 ↔ [ 𝐴 ] 𝑅 ≠ ∅ ) )
13 1 5 12 pm5.21nii ⊢ ( 𝐴 ∈ dom 𝑅 ↔ [ 𝐴 ] 𝑅 ≠ ∅ )