Theorem dm0rn0 5873

Description: An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998.) Avoid ax-10 2147, ax-11 2163, ax-12 2185. (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 5089	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑦))
2		breq2 5090	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑧𝐴𝑦 ↔ 𝑧𝐴𝑤))
3	1, 2	excomw 2048	. . . . . . 7 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑦∃𝑧 𝑧𝐴𝑦)
4		breq2 5090	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑥𝐴𝑦 ↔ 𝑥𝐴𝑤))
5	1, 4	sylan9bbr 510	. . . . . . . 8 ⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑥) → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑤))
6	5	cbvex2vw 2043	. . . . . . 7 ⊢ (∃𝑦∃𝑧 𝑧𝐴𝑦 ↔ ∃𝑤∃𝑥 𝑥𝐴𝑤)
7	3, 6	bitri 275	. . . . . 6 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑤∃𝑥 𝑥𝐴𝑤)
8	7	notbii 320	. . . . 5 ⊢ (¬ ∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ¬ ∃𝑤∃𝑥 𝑥𝐴𝑤)
9		alnex 1783	. . . . 5 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ¬ ∃𝑧∃𝑦 𝑧𝐴𝑦)
10		alnex 1783	. . . . 5 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ¬ ∃𝑤∃𝑥 𝑥𝐴𝑤)
11	8, 9, 10	3bitr4i 303	. . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤)
12		noel 4279	. . . . . 6 ⊢ ¬ 𝑧 ∈ ∅
13	12	nbn 372	. . . . 5 ⊢ (¬ ∃𝑦 𝑧𝐴𝑦 ↔ (∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
14	13	albii 1821	. . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
15		noel 4279	. . . . . 6 ⊢ ¬ 𝑤 ∈ ∅
16	15	nbn 372	. . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑤 ↔ (∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
17	16	albii 1821	. . . 4 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
18	11, 14, 17	3bitr3i 301	. . 3 ⊢ (∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅) ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
19		breq1 5089	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥𝐴𝑦 ↔ 𝑧𝐴𝑦))
20	19	exbidv 1923	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦 𝑧𝐴𝑦))
21	20	eqabcbw 2811	. . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
22	4	exbidv 1923	. . . 4 ⊢ (𝑦 = 𝑤 → (∃𝑥 𝑥𝐴𝑦 ↔ ∃𝑥 𝑥𝐴𝑤))
23	22	eqabcbw 2811	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
24	18, 21, 23	3bitr4i 303	. 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
25		df-dm 5634	. . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
26	25	eqeq1i 2742	. 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
27		dfrn2 5837	. . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
28	27	eqeq1i 2742	. 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
29	24, 26, 28	3bitr4i 303	1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715  ∅c0 4274   class class class wbr 5086  dom cdm 5624  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  rn0  5875  relrn0  5922  imadisj  6039  rnsnn0  6166  rnmpt0f  6201  f00  6716  f0rn0  6719  2nd0  7942  iinon  8273  onoviun  8276  onnseq  8277  map0b  8824  fodomfib  9232  fodomfibOLD  9234  intrnfi  9322  wdomtr  9483  noinfep  9572  wemapwe  9609  fin23lem31  10256  fin23lem40  10264  isf34lem7  10292  isf34lem6  10293  ttukeylem6  10427  fodomb  10439  rpnnen1lem4  12921  rpnnen1lem5  12922  fseqsupcl  13930  fseqsupubi  13931  dmtrclfv  14971  ruclem11  16198  prmreclem6  16883  0ram  16982  0ram2  16983  0ramcl  16985  gsumval2  18645  ghmrn  19195  gexex  19819  gsumval3  19873  subdrgint  20771  iinopn  22877  hauscmplem  23381  fbasrn  23859  alexsublem  24019  evth  24936  minveclem1  25401  minveclem3b  25405  ovollb2  25466  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovoliun2  25483  ioombl1lem4  25538  uniioombllem1  25558  uniioombllem2  25560  uniioombllem6  25565  mbfsup  25641  mbfinf  25642  mbflimsup  25643  itg1climres  25691  itg2monolem1  25727  itg2mono  25730  itg2i1fseq2  25733  itg2cnlem1  25738  minvecolem1  30960  rge0scvg  34109  esumpcvgval  34238  cvmsss2  35472  fin2so  37942  ptrecube  37955  heicant  37990  isbnd3  38119  totbndbnd  38124  rnnonrel  44036  stoweidlem35  46481  hoicvr  46994