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 𝐴 = { 𝑥 ∣ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		df-dm	⊢ dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }
2		df-br	⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
3	2	exbii	⊢ ( ∃ 𝑦 𝑥 𝐴 𝑦 ↔ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
4	3	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 } = { 𝑥 ∣ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }
5	1 4	eqtri	⊢ dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 }