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

Metamath Proof Explorer

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