Theorem dm0rn0 5831

Description: An empty domain is equivalent to an empty range. (Contributed by NM, 21-May-1998.)

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		alnex 1787	. . . . . 6 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥∃𝑦 𝑥𝐴𝑦)
2		excom 2165	. . . . . 6 ⊢ (∃𝑥∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦∃𝑥 𝑥𝐴𝑦)
3	1, 2	xchbinx 333	. . . . 5 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦)
4		alnex 1787	. . . . 5 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦)
5	3, 4	bitr4i 277	. . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦)
6		noel 4269	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
7	6	nbn 372	. . . . 5 ⊢ (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
8	7	albii 1825	. . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
9		noel 4269	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
10	9	nbn 372	. . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
11	10	albii 1825	. . . 4 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
12	5, 8, 11	3bitr3i 300	. . 3 ⊢ (∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
13		abeq1 2874	. . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
14		abeq1 2874	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
15	12, 13, 14	3bitr4i 302	. 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
16		df-dm 5598	. . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
17	16	eqeq1i 2744	. 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
18		dfrn2 5794	. . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
19	18	eqeq1i 2744	. 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
20	15, 17, 19	3bitr4i 302	1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1539   = wceq 1541  ∃wex 1785   ∈ wcel 2109  {cab 2716  ∅c0 4261   class class class wbr 5078  dom cdm 5588  ran crn 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-cnv 5596  df-dm 5598  df-rn 5599

This theorem is referenced by:  rn0  5832  relrn0  5875  imadisj  5985  rnsnn0  6108  rnmpt0f  6143  f00  6652  f0rn0  6655  2nd0  7824  iinon  8155  onoviun  8158  onnseq  8159  map0b  8645  fodomfib  9054  intrnfi  9136  wdomtr  9295  noinfep  9379  wemapwe  9416  fin23lem31  10083  fin23lem40  10091  isf34lem7  10119  isf34lem6  10120  ttukeylem6  10254  fodomb  10266  rpnnen1lem4  12702  rpnnen1lem5  12703  fseqsupcl  13678  fseqsupubi  13679  dmtrclfv  14710  ruclem11  15930  prmreclem6  16603  0ram  16702  0ram2  16703  0ramcl  16705  gsumval2  18351  ghmrn  18828  gexex  19435  gsumval3  19489  subdrgint  20052  iinopn  22032  hauscmplem  22538  fbasrn  23016  alexsublem  23176  evth  24103  minveclem1  24569  minveclem3b  24573  ovollb2  24634  ovolunlem1a  24641  ovolunlem1  24642  ovoliunlem1  24647  ovoliun2  24651  ioombl1lem4  24706  uniioombllem1  24726  uniioombllem2  24728  uniioombllem6  24733  mbfsup  24809  mbfinf  24810  mbflimsup  24811  itg1climres  24860  itg2monolem1  24896  itg2mono  24899  itg2i1fseq2  24902  itg2cnlem1  24907  minvecolem1  29215  rge0scvg  31878  esumpcvgval  32025  cvmsss2  33215  fin2so  35743  ptrecube  35756  heicant  35791  isbnd3  35921  totbndbnd  35926  rnnonrel  41152  stoweidlem35  43530  hoicvr  44040