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

Metamath Proof Explorer

Definition df-domain

Description: Define the domain function. See brdomain for its value. (Contributed by Scott Fenton, 11-Apr-2014)

		Ref	Expression
	Assertion	df-domain	$⊢ 𝖣𝗈𝗆𝖺𝗂𝗇 = 𝖨𝗆𝖺𝗀𝖾 ({1^{st} ↾}_{(V \times V)})$

Step	Hyp	Ref	Expression
0		cdomain	$class 𝖣𝗈𝗆𝖺𝗂𝗇$
1		c1st	$class 1^{st}$
2		cvv	$class V$
3	2 2	cxp	$class (V \times V)$
4	1 3	cres	$class ({1^{st} ↾}_{(V \times V)})$
5	4	cimage	$class 𝖨𝗆𝖺𝗀𝖾 ({1^{st} ↾}_{(V \times V)})$
6	0 5	wceq	$wff 𝖣𝗈𝗆𝖺𝗂𝗇 = 𝖨𝗆𝖺𝗀𝖾 ({1^{st} ↾}_{(V \times V)})$