# Metamath Proof Explorer

## Theorem dm0rn0

Description: An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998)

Ref Expression
Assertion dm0rn0
`|- ( dom A = (/) <-> ran A = (/) )`

### Proof

Step Hyp Ref Expression
1 alnex
` |-  ( A. x -. E. y x A y <-> -. E. x E. y x A y )`
2 excom
` |-  ( E. x E. y x A y <-> E. y E. x x A y )`
3 1 2 xchbinx
` |-  ( A. x -. E. y x A y <-> -. E. y E. x x A y )`
4 alnex
` |-  ( A. y -. E. x x A y <-> -. E. y E. x x A y )`
5 3 4 bitr4i
` |-  ( A. x -. E. y x A y <-> A. y -. E. x x A y )`
6 noel
` |-  -. x e. (/)`
7 6 nbn
` |-  ( -. E. y x A y <-> ( E. y x A y <-> x e. (/) ) )`
8 7 albii
` |-  ( A. x -. E. y x A y <-> A. x ( E. y x A y <-> x e. (/) ) )`
9 noel
` |-  -. y e. (/)`
10 9 nbn
` |-  ( -. E. x x A y <-> ( E. x x A y <-> y e. (/) ) )`
11 10 albii
` |-  ( A. y -. E. x x A y <-> A. y ( E. x x A y <-> y e. (/) ) )`
12 5 8 11 3bitr3i
` |-  ( A. x ( E. y x A y <-> x e. (/) ) <-> A. y ( E. x x A y <-> y e. (/) ) )`
13 abeq1
` |-  ( { x | E. y x A y } = (/) <-> A. x ( E. y x A y <-> x e. (/) ) )`
14 abeq1
` |-  ( { y | E. x x A y } = (/) <-> A. y ( E. x x A y <-> y e. (/) ) )`
15 12 13 14 3bitr4i
` |-  ( { x | E. y x A y } = (/) <-> { y | E. x x A y } = (/) )`
16 df-dm
` |-  dom A = { x | E. y x A y }`
17 16 eqeq1i
` |-  ( dom A = (/) <-> { x | E. y x A y } = (/) )`
18 dfrn2
` |-  ran A = { y | E. x x A y }`
19 18 eqeq1i
` |-  ( ran A = (/) <-> { y | E. x x A y } = (/) )`
20 15 17 19 3bitr4i
` |-  ( dom A = (/) <-> ran A = (/) )`