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

Metamath Proof Explorer

Definition df-dm

Description: Define the domain of a class. Definition 3 of Suppes p. 59. For example, F = { <. 2 , 6 >. , <. 3 , 9 >. } -> dom F = { 2 , 3 } ( ex-dm ). Another example is the domain of the complex arctangent, ( A e. dom arctan <-> ( A e. CC /\ A =/= -ui /\ A =/= i ) ) (for proof see atandm ). Contrast with range (defined in df-rn ). For alternate definitions see dfdm2 , dfdm3 , and dfdm4 . The notation " dom " is used by Enderton; other authors sometimes use script D. (Contributed by NM, 1-Aug-1994)

		Ref	Expression
	Assertion	df-dm	⊢ dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	cdm	⊢ dom 𝐴
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4	2	cv	⊢ 𝑥
5	3	cv	⊢ 𝑦
6	4 5 0	wbr	⊢ 𝑥 𝐴 𝑦
7	6 3	wex	⊢ ∃ 𝑦 𝑥 𝐴 𝑦
8	7 2	cab	⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }
9	1 8	wceq	⊢ dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }