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

Metamath Proof Explorer

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 𝑅 = { 𝑥 ∣ [ 𝑥 ] 𝑅 ≠ ∅ }