Theorem dm0rn0 5879

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 5088	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧𝐴𝑦 ↔ 𝑥𝐴𝑦))
2		breq2 5089	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (𝑧𝐴𝑦 ↔ 𝑧𝐴𝑤))
3	1, 2	excomw 2048	. . . . . . 7 ⊢ (∃𝑧∃𝑦 𝑧𝐴𝑦 ↔ ∃𝑦∃𝑧 𝑧𝐴𝑦)
4		breq2 5089	. . . . . . . . 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 4278	. . . . . 6 ⊢ ¬ 𝑧 ∈ ∅
13	12	nbn 372	. . . . 5 ⊢ (¬ ∃𝑦 𝑧𝐴𝑦 ↔ (∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
14	13	albii 1821	. . . 4 ⊢ (∀𝑧 ¬ ∃𝑦 𝑧𝐴𝑦 ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
15		noel 4278	. . . . . 6 ⊢ ¬ 𝑤 ∈ ∅
16	15	nbn 372	. . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑤 ↔ (∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
17	16	albii 1821	. . . 4 ⊢ (∀𝑤 ¬ ∃𝑥 𝑥𝐴𝑤 ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
18	11, 14, 17	3bitr3i 301	. . 3 ⊢ (∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅) ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
19		breq1 5088	. . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥𝐴𝑦 ↔ 𝑧𝐴𝑦))
20	19	exbidv 1923	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦 𝑧𝐴𝑦))
21	20	eqabcbw 2810	. . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑧(∃𝑦 𝑧𝐴𝑦 ↔ 𝑧 ∈ ∅))
22	4	exbidv 1923	. . . 4 ⊢ (𝑦 = 𝑤 → (∃𝑥 𝑥𝐴𝑦 ↔ ∃𝑥 𝑥𝐴𝑤))
23	22	eqabcbw 2810	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑤(∃𝑥 𝑥𝐴𝑤 ↔ 𝑤 ∈ ∅))
24	18, 21, 23	3bitr4i 303	. 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
25		df-dm 5641	. . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
26	25	eqeq1i 2741	. 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
27		dfrn2 5843	. . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
28	27	eqeq1i 2741	. 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 2714  ∅c0 4273   class class class wbr 5085  dom cdm 5631  ran crn 5632

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  rn0  5881  relrn0  5928  imadisj  6045  rnsnn0  6172  rnmpt0f  6207  f00  6722  f0rn0  6725  2nd0  7949  iinon  8280  onoviun  8283  onnseq  8284  map0b  8831  fodomfib  9239  fodomfibOLD  9241  intrnfi  9329  wdomtr  9490  noinfep  9581  wemapwe  9618  fin23lem31  10265  fin23lem40  10273  isf34lem7  10301  isf34lem6  10302  ttukeylem6  10436  fodomb  10448  rpnnen1lem4  12930  rpnnen1lem5  12931  fseqsupcl  13939  fseqsupubi  13940  dmtrclfv  14980  ruclem11  16207  prmreclem6  16892  0ram  16991  0ram2  16992  0ramcl  16994  gsumval2  18654  ghmrn  19204  gexex  19828  gsumval3  19882  subdrgint  20780  iinopn  22867  hauscmplem  23371  fbasrn  23849  alexsublem  24009  evth  24926  minveclem1  25391  minveclem3b  25395  ovollb2  25456  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliun2  25473  ioombl1lem4  25528  uniioombllem1  25548  uniioombllem2  25550  uniioombllem6  25555  mbfsup  25631  mbfinf  25632  mbflimsup  25633  itg1climres  25681  itg2monolem1  25717  itg2mono  25720  itg2i1fseq2  25723  itg2cnlem1  25728  minvecolem1  30945  rge0scvg  34093  esumpcvgval  34222  cvmsss2  35456  fin2so  37928  ptrecube  37941  heicant  37976  isbnd3  38105  totbndbnd  38110  rnnonrel  44018  stoweidlem35  46463  hoicvr  46976