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	⊢ Ⅎ 𝑥 𝐴
	dfdmf.2	⊢ Ⅎ 𝑦 𝐴
Assertion	dfdmf	⊢ dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }

Proof

Step	Hyp	Ref	Expression
1		dfdmf.1	⊢ Ⅎ 𝑥 𝐴
2		dfdmf.2	⊢ Ⅎ 𝑦 𝐴
3		df-dm	⊢ dom 𝐴 = { 𝑤 ∣ ∃ 𝑣 𝑤 𝐴 𝑣 }
4		nfcv	⊢ Ⅎ 𝑦 𝑤
5		nfcv	⊢ Ⅎ 𝑦 𝑣
6	4 2 5	nfbr	⊢ Ⅎ 𝑦 𝑤 𝐴 𝑣
7		nfv	⊢ Ⅎ 𝑣 𝑤 𝐴 𝑦
8		breq2	⊢ ( 𝑣 = 𝑦 → ( 𝑤 𝐴 𝑣 ↔ 𝑤 𝐴 𝑦 ) )
9	6 7 8	cbvexv1	⊢ ( ∃ 𝑣 𝑤 𝐴 𝑣 ↔ ∃ 𝑦 𝑤 𝐴 𝑦 )
10	9	abbii	⊢ { 𝑤 ∣ ∃ 𝑣 𝑤 𝐴 𝑣 } = { 𝑤 ∣ ∃ 𝑦 𝑤 𝐴 𝑦 }
11		nfcv	⊢ Ⅎ 𝑥 𝑤
12		nfcv	⊢ Ⅎ 𝑥 𝑦
13	11 1 12	nfbr	⊢ Ⅎ 𝑥 𝑤 𝐴 𝑦
14	13	nfex	⊢ Ⅎ 𝑥 ∃ 𝑦 𝑤 𝐴 𝑦
15		nfv	⊢ Ⅎ 𝑤 ∃ 𝑦 𝑥 𝐴 𝑦
16		breq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝐴 𝑦 ↔ 𝑥 𝐴 𝑦 ) )
17	16	exbidv	⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑦 𝑤 𝐴 𝑦 ↔ ∃ 𝑦 𝑥 𝐴 𝑦 ) )
18	14 15 17	cbvabw	⊢ { 𝑤 ∣ ∃ 𝑦 𝑤 𝐴 𝑦 } = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }
19	3 10 18	3eqtri	⊢ dom 𝐴 = { 𝑥 ∣ ∃ 𝑦 𝑥 𝐴 𝑦 }