Theorem dm0rn0 5896

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

Assertion

Ref	Expression
dm0rn0	⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)

Proof of Theorem dm0rn0

Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5100	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑦))
2		breq2 5101	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑧𝐴𝑦 ↔ 𝑧𝐴𝑤))
3	1, 2	excomw 2065	. . . . . . 7 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑦∃𝑧 𝑧𝐴𝑦)
4		breq2 5101	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑥𝐴𝑦 ↔ 𝑥𝐴𝑤))
5	1, 4	sylan9bbr 518	. . . . . . . 8 ⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑥) → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑤))
6	5	cbvex2vw 2060	. . . . . . 7 ⊢ (∃𝑦∃𝑧 𝑧𝐴𝑦 ↔ ∃𝑤∃𝑥 𝑥𝐴𝑤)
7	3, 6	bitri 277	. . . . . 6 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑤∃𝑥 𝑥𝐴𝑤)
8	7	notbii 322	. . . . 5 ⊢ (¬ ∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ¬ ∃𝑤∃𝑥 𝑥𝐴𝑤)
9		alnex 1800	. . . . 5 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ¬ ∃𝑧∃𝑦 𝑧𝐴𝑦)
10		alnex 1800	. . . . 5 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ¬ ∃𝑤∃𝑥 𝑥𝐴𝑤)
11	8, 9, 10	3bitr4i 305	. . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤)
12		noel 4288	. . . . . 6 ⊢ ¬ 𝑧 ∈ ∅
13	12	nbn 374	. . . . 5 ⊢ (¬ ∃𝑦 𝑧𝐴𝑦 ↔ (∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
14	13	albii 1838	. . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
15		noel 4288	. . . . . 6 ⊢ ¬ 𝑤 ∈ ∅
16	15	nbn 374	. . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑤 ↔ (∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
17	16	albii 1838	. . . 4 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
18	11, 14, 17	3bitr3i 303	. . 3 ⊢ (∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅) ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
19		breq1 5100	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥𝐴𝑦 ↔ 𝑧𝐴𝑦))
20	19	exbidv 1940	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦 𝑧𝐴𝑦))
21	20	eqabcbw 2835	. . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
22	4	exbidv 1940	. . . 4 ⊢ (𝑦 = 𝑤 → (∃𝑥 𝑥𝐴𝑦 ↔ ∃𝑥 𝑥𝐴𝑤))
23	22	eqabcbw 2835	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
24	18, 21, 23	3bitr4i 305	. 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
25		df-dm 5653	. . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
26	25	eqeq1i 2766	. 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
27		dfrn2 5860	. . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
28	27	eqeq1i 2766	. 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
29	24, 26, 28	3bitr4i 305	1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 208  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141  {cab 2739  ∅c0 4283   class class class wbr 5097  dom cdm 5643  ran crn 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-cnv 5651  df-dm 5653  df-rn 5654

This theorem is referenced by:  rn0  5898  relrn0  5945  imadisj  6064  rnsnn0  6189  rnmpt0f  6224  f00  6740  f0rn0  6743  2nd0  7971  iinon  8304  onoviun  8307  onnseq  8308  map0b  8858  fodomfib  9266  fodomfibOLD  9267  intrnfi  9355  wdomtr  9516  noinfep  9608  wemapwe  9645  fin23lem31  10293  fin23lem40  10301  isf34lem7  10329  isf34lem6  10330  ttukeylem6  10464  fodomb  10476  rpnnen1lem4  12974  rpnnen1lem5  12975  fseqsupcl  13983  fseqsupubi  13984  dmtrclfv  15024  ruclem11  16262  prmreclem6  16947  0ram  17046  0ram2  17047  0ramcl  17049  gsumval2  18710  ghmrn  19259  gexex  19883  gsumval3  19937  subdrgint  20839  iinopn  22949  hauscmplem  23453  fbasrn  23931  alexsublem  24091  evth  25008  minveclem1  25473  minveclem3b  25477  ovollb2  25538  ovolunlem1a  25545  ovolunlem1  25546  ovoliunlem1  25551  ovoliun2  25555  ioombl1lem4  25610  uniioombllem1  25630  uniioombllem2  25632  uniioombllem6  25637  mbfsup  25713  mbfinf  25714  mbflimsup  25715  itg1climres  25763  itg2monolem1  25799  itg2mono  25802  itg2i1fseq2  25805  itg2cnlem1  25810  minvecolem1  31033  rge0scvg  34206  esumpcvgval  34335  cvmsss2  35584  fin2so  38066  ptrecube  38079  heicant  38114  isbnd3  38243  totbndbnd  38248  rnnonrel  44127  stoweidlem35  46569  hoicvr  47082