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 = (/) )