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

Metamath Proof Explorer

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 }