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