Theorem dm0rn0

Description: An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998) Avoid ax-10 , ax-11 , ax-12 . (Revised by TM, 24-Jan-2026)

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

Proof

Step	Hyp	Ref	Expression
1		breq1	|- ( z = x -> ( z A y <-> x A y ) )
2		breq2	|- ( y = w -> ( z A y <-> z A w ) )
3	1 2	excomw	|- ( E. z E. y z A y <-> E. y E. z z A y )
4		breq2	|- ( y = w -> ( x A y <-> x A w ) )
5	1 4	sylan9bbr	|- ( ( y = w /\ z = x ) -> ( z A y <-> x A w ) )
6	5	cbvex2vw	|- ( E. y E. z z A y <-> E. w E. x x A w )
7	3 6	bitri	|- ( E. z E. y z A y <-> E. w E. x x A w )
8	7	notbii	|- ( -. E. z E. y z A y <-> -. E. w E. x x A w )
9		alnex	|- ( A. z -. E. y z A y <-> -. E. z E. y z A y )
10		alnex	|- ( A. w -. E. x x A w <-> -. E. w E. x x A w )
11	8 9 10	3bitr4i	|- ( A. z -. E. y z A y <-> A. w -. E. x x A w )
12		noel	|- -. z e. (/)
13	12	nbn	|- ( -. E. y z A y <-> ( E. y z A y <-> z e. (/) ) )
14	13	albii	|- ( A. z -. E. y z A y <-> A. z ( E. y z A y <-> z e. (/) ) )
15		noel	|- -. w e. (/)
16	15	nbn	|- ( -. E. x x A w <-> ( E. x x A w <-> w e. (/) ) )
17	16	albii	|- ( A. w -. E. x x A w <-> A. w ( E. x x A w <-> w e. (/) ) )
18	11 14 17	3bitr3i	|- ( A. z ( E. y z A y <-> z e. (/) ) <-> A. w ( E. x x A w <-> w e. (/) ) )
19		breq1	|- ( x = z -> ( x A y <-> z A y ) )
20	19	exbidv	|- ( x = z -> ( E. y x A y <-> E. y z A y ) )
21	20	eqabcbw	|- ( { x | E. y x A y } = (/) <-> A. z ( E. y z A y <-> z e. (/) ) )
22	4	exbidv	|- ( y = w -> ( E. x x A y <-> E. x x A w ) )
23	22	eqabcbw	|- ( { y | E. x x A y } = (/) <-> A. w ( E. x x A w <-> w e. (/) ) )
24	18 21 23	3bitr4i	|- ( { x | E. y x A y } = (/) <-> { y | E. x x A y } = (/) )
25		df-dm	|- dom A = { x | E. y x A y }
26	25	eqeq1i	|- ( dom A = (/) <-> { x | E. y x A y } = (/) )
27		dfrn2	|- ran A = { y | E. x x A y }
28	27	eqeq1i	|- ( ran A = (/) <-> { y | E. x x A y } = (/) )
29	24 26 28	3bitr4i	|- ( dom A = (/) <-> ran A = (/) )