Theorem dm0rn0 5881

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 5103	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑦))
2		breq2 5104	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑧𝐴𝑦 ↔ 𝑧𝐴𝑤))
3	1, 2	excomw 2048	. . . . . . 7 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑦∃𝑧 𝑧𝐴𝑦)
4		breq2 5104	. . . . . . . . 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 4292	. . . . . 6 ⊢ ¬ 𝑧 ∈ ∅
13	12	nbn 372	. . . . 5 ⊢ (¬ ∃𝑦 𝑧𝐴𝑦 ↔ (∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
14	13	albii 1821	. . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
15		noel 4292	. . . . . 6 ⊢ ¬ 𝑤 ∈ ∅
16	15	nbn 372	. . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑤 ↔ (∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
17	16	albii 1821	. . . 4 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
18	11, 14, 17	3bitr3i 301	. . 3 ⊢ (∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅) ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
19		breq1 5103	. . . . 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 5642	. . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
26	25	eqeq1i 2742	. 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
27		dfrn2 5845	. . 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 4287   class class class wbr 5100  dom cdm 5632  ran crn 5633

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  rn0  5883  relrn0  5930  imadisj  6047  rnsnn0  6174  rnmpt0f  6209  f00  6724  f0rn0  6727  2nd0  7950  iinon  8282  onoviun  8285  onnseq  8286  map0b  8833  fodomfib  9241  fodomfibOLD  9243  intrnfi  9331  wdomtr  9492  noinfep  9581  wemapwe  9618  fin23lem31  10265  fin23lem40  10273  isf34lem7  10301  isf34lem6  10302  ttukeylem6  10436  fodomb  10448  rpnnen1lem4  12905  rpnnen1lem5  12906  fseqsupcl  13912  fseqsupubi  13913  dmtrclfv  14953  ruclem11  16177  prmreclem6  16861  0ram  16960  0ram2  16961  0ramcl  16963  gsumval2  18623  ghmrn  19170  gexex  19794  gsumval3  19848  subdrgint  20748  iinopn  22858  hauscmplem  23362  fbasrn  23840  alexsublem  24000  evth  24926  minveclem1  25392  minveclem3b  25396  ovollb2  25458  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliun2  25475  ioombl1lem4  25530  uniioombllem1  25550  uniioombllem2  25552  uniioombllem6  25557  mbfsup  25633  mbfinf  25634  mbflimsup  25635  itg1climres  25683  itg2monolem1  25719  itg2mono  25722  itg2i1fseq2  25725  itg2cnlem1  25730  minvecolem1  30961  rge0scvg  34126  esumpcvgval  34255  cvmsss2  35487  fin2so  37855  ptrecube  37868  heicant  37903  isbnd3  38032  totbndbnd  38037  rnnonrel  43944  stoweidlem35  46390  hoicvr  46903