Theorem dm0rn0 5908

Description: An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998.) Avoid ax-10 2178, ax-11 2194, ax-12 2213. (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 5106	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑦))
2		breq2 5107	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑧𝐴𝑦 ↔ 𝑧𝐴𝑤))
3	1, 2	excomw 2079	. . . . . . 7 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑦∃𝑧 𝑧𝐴𝑦)
4		breq2 5107	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → (𝑥𝐴𝑦 ↔ 𝑥𝐴𝑤))
5	1, 4	sylan9bbr 520	. . . . . . . 8 ⊢ ((𝑦 = 𝑤 ∧ 𝑧 = 𝑥) → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑤))
6	5	cbvex2vw 2074	. . . . . . 7 ⊢ (∃𝑦∃𝑧 𝑧𝐴𝑦 ↔ ∃𝑤∃𝑥 𝑥𝐴𝑤)
7	3, 6	bitri 278	. . . . . 6 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑤∃𝑥 𝑥𝐴𝑤)
8	7	notbii 323	. . . . 5 ⊢ (¬ ∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ¬ ∃𝑤∃𝑥 𝑥𝐴𝑤)
9		alnex 1814	. . . . 5 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ¬ ∃𝑧∃𝑦 𝑧𝐴𝑦)
10		alnex 1814	. . . . 5 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ¬ ∃𝑤∃𝑥 𝑥𝐴𝑤)
11	8, 9, 10	3bitr4i 306	. . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤)
12		noel 4284	. . . . . 6 ⊢ ¬ 𝑧 ∈ ∅
13	12	nbn 375	. . . . 5 ⊢ (¬ ∃𝑦 𝑧𝐴𝑦 ↔ (∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
14	13	albii 1852	. . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
15		noel 4284	. . . . . 6 ⊢ ¬ 𝑤 ∈ ∅
16	15	nbn 375	. . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑤 ↔ (∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
17	16	albii 1852	. . . 4 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
18	11, 14, 17	3bitr3i 304	. . 3 ⊢ (∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅) ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
19		breq1 5106	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥𝐴𝑦 ↔ 𝑧𝐴𝑦))
20	19	exbidv 1954	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦 𝑧𝐴𝑦))
21	20	eqabcbw 2834	. . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
22	4	exbidv 1954	. . . 4 ⊢ (𝑦 = 𝑤 → (∃𝑥 𝑥𝐴𝑦 ↔ ∃𝑥 𝑥𝐴𝑤))
23	22	eqabcbw 2834	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
24	18, 21, 23	3bitr4i 306	. 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
25		df-dm 5665	. . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
26	25	eqeq1i 2765	. 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
27		dfrn2 5872	. . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
28	27	eqeq1i 2765	. 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
29	24, 26, 28	3bitr4i 306	1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2738  ∅c0 4279   class class class wbr 5103  dom cdm 5655  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  rn0  5910  relrn0  5957  imadisj  6076  rnsnn0  6204  rnmpt0f  6239  f00  6758  f0rn0  6761  2nd0  7994  iinon  8330  onoviun  8333  onnseq  8334  map0b  8891  fodomfib  9299  intrnfi  9387  wdomtr  9548  noinfep  9640  wemapwe  9677  fin23lem31  10346  fin23lem40  10354  isf34lem7  10382  isf34lem6  10383  ttukeylem6  10517  fodomb  10530  rpnnen1lem4  13031  rpnnen1lem5  13032  fseqsupcl  14042  fseqsupubi  14043  dmtrclfv  15092  ruclem11  16329  prmreclem6  17014  0ram  17113  0ram2  17114  0ramcl  17116  gsumval2  18789  ghmrn  19357  gexex  19981  gsumval3  20035  subdrgint  20970  iinopn  23128  hauscmplem  23632  fbasrn  24111  alexsublem  24271  evth  25188  minveclem1  25653  minveclem3b  25657  ovollb2  25718  ovolunlem1a  25725  ovolunlem1  25726  ovoliunlem1  25731  ovoliun2  25735  ioombl1lem4  25790  uniioombllem1  25810  uniioombllem2  25812  uniioombllem6  25817  mbfsup  25893  mbfinf  25894  mbflimsup  25895  itg1climres  25943  itg2monolem1  25979  itg2mono  25982  itg2i1fseq2  25985  itg2cnlem1  25990  minvecolem1  31356  rge0scvg  34460  esumpcvgval  34589  cvmsss2  35854  fin2so  38362  ptrecube  38370  heicant  38405  isbnd3  38535  totbndbnd  38540  rnnonrel  44432  stoweidlem35  46864  hoicvr  47377