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

Metamath Proof Explorer

Theorem dfdm3

Description: Alternate definition of domain. Definition 6.5(1) of TakeutiZaring p. 24. (Contributed by NM, 28-Dec-1996)

Ref Expression
Assertion dfdm3 ⊢ dom ⁡ A = x | ∃ y x y ∈ A

Proof

Step Hyp Ref Expression
1 df-dm ⊢ dom ⁡ A = x | ∃ y x A y
2 df-br ⊢ x A y ↔ x y ∈ A
3 2 exbii ⊢ ∃ y x A y ↔ ∃ y x y ∈ A
4 3 abbii ⊢ x | ∃ y x A y = x | ∃ y x y ∈ A
5 1 4 eqtri ⊢ dom ⁡ A = x | ∃ y x y ∈ A