Theorem dfdm6

Description: Alternate definition of domain. (Contributed by Peter Mazsa, 2-Mar-2018)

	Ref	Expression
Assertion	dfdm6	⊢ dom 𝑅 = { 𝑥 ∣ [ 𝑥 ] 𝑅 ≠ ∅ }

Proof

Step	Hyp	Ref	Expression
1		ecdmn0	⊢ ( 𝑥 ∈ dom 𝑅 ↔ [ 𝑥 ] 𝑅 ≠ ∅ )
2	1	eqabi	⊢ dom 𝑅 = { 𝑥 ∣ [ 𝑥 ] 𝑅 ≠ ∅ }