Theorem dfdmf

Description: Definition of domain, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Mar-1995) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	dfdmf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	dfdmf.2	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	dfdmf	$$⊢\mathrm{dom}A=\left\{x|\exists yxAy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfdmf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		dfdmf.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		df-dm	$$⊢\mathrm{dom}A=\left\{w|\exists vwAv\right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yw$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yv$$
6	4 2 5	nfbr	$$⊢ℲywAv$$
7		nfv	$$⊢ℲvwAy$$
8		breq2	$$⊢v=y\to \left(wAv\leftrightarrow wAy\right)$$
9	6 7 8	cbvexv1	$$⊢\exists vwAv\leftrightarrow \exists ywAy$$
10	9	abbii	$$⊢\left\{w|\exists vwAv\right\}=\left\{w|\exists ywAy\right\}$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
13	11 1 12	nfbr	$$⊢ℲxwAy$$
14	13	nfex	$$⊢Ⅎx\exists ywAy$$
15		nfv	$$⊢Ⅎw\exists yxAy$$
16		breq1	$$⊢w=x\to \left(wAy\leftrightarrow xAy\right)$$
17	16	exbidv	$$⊢w=x\to \left(\exists ywAy\leftrightarrow \exists yxAy\right)$$
18	14 15 17	cbvabw	$$⊢\left\{w|\exists ywAy\right\}=\left\{x|\exists yxAy\right\}$$
19	3 10 18	3eqtri	$$⊢\mathrm{dom}A=\left\{x|\exists yxAy\right\}$$