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	|- F/_ x A
	dfdmf.2	|- F/_ y A
Assertion	dfdmf	|- dom A = { x | E. y x A y }

Proof

Step	Hyp	Ref	Expression
1		dfdmf.1	|- F/_ x A
2		dfdmf.2	|- F/_ y A
3		df-dm	|- dom A = { w | E. v w A v }
4		nfcv	|- F/_ y w
5		nfcv	|- F/_ y v
6	4 2 5	nfbr	|- F/ y w A v
7		nfv	|- F/ v w A y
8		breq2	|- ( v = y -> ( w A v <-> w A y ) )
9	6 7 8	cbvexv1	|- ( E. v w A v <-> E. y w A y )
10	9	abbii	|- { w | E. v w A v } = { w | E. y w A y }
11		nfcv	|- F/_ x w
12		nfcv	|- F/_ x y
13	11 1 12	nfbr	|- F/ x w A y
14	13	nfex	|- F/ x E. y w A y
15		nfv	|- F/ w E. y x A y
16		breq1	|- ( w = x -> ( w A y <-> x A y ) )
17	16	exbidv	|- ( w = x -> ( E. y w A y <-> E. y x A y ) )
18	14 15 17	cbvabw	|- { w | E. y w A y } = { x | E. y x A y }
19	3 10 18	3eqtri	|- dom A = { x | E. y x A y }