Theorem dm0rn0 5827

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 1784	. . . . . 6 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥∃𝑦 𝑥𝐴𝑦)
2		excom 2162	. . . . . 6 ⊢ (∃𝑥∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦∃𝑥 𝑥𝐴𝑦)
3	1, 2	xchbinx 334	. . . . 5 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦)
4		alnex 1784	. . . . 5 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦)
5	3, 4	bitr4i 277	. . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦)
6		noel 4264	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
7	6	nbn 373	. . . . 5 ⊢ (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
8	7	albii 1822	. . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
9		noel 4264	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
10	9	nbn 373	. . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
11	10	albii 1822	. . . 4 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
12	5, 8, 11	3bitr3i 301	. . 3 ⊢ (∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
13		abeq1 2873	. . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
14		abeq1 2873	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
15	12, 13, 14	3bitr4i 303	. 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
16		df-dm 5594	. . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
17	16	eqeq1i 2743	. 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
18		dfrn2 5790	. . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
19	18	eqeq1i 2743	. 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
20	15, 17, 19	3bitr4i 303	1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106  {cab 2715  ∅c0 4256   class class class wbr 5073  dom cdm 5584  ran crn 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pr 5350

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3431  df-dif 3889  df-un 3891  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5074  df-opab 5136  df-cnv 5592  df-dm 5594  df-rn 5595

This theorem is referenced by:  rn0  5828  relrn0  5871  imadisj  5981  rnsnn0  6104  rnmpt0f  6139  f00  6648  f0rn0  6651  2nd0  7827  iinon  8158  onoviun  8161  onnseq  8162  map0b  8658  fodomfib  9080  intrnfi  9162  wdomtr  9321  noinfep  9405  wemapwe  9442  fin23lem31  10109  fin23lem40  10117  isf34lem7  10145  isf34lem6  10146  ttukeylem6  10280  fodomb  10292  rpnnen1lem4  12730  rpnnen1lem5  12731  fseqsupcl  13707  fseqsupubi  13708  dmtrclfv  14739  ruclem11  15959  prmreclem6  16632  0ram  16731  0ram2  16732  0ramcl  16734  gsumval2  18380  ghmrn  18857  gexex  19464  gsumval3  19518  subdrgint  20081  iinopn  22061  hauscmplem  22567  fbasrn  23045  alexsublem  23205  evth  24132  minveclem1  24598  minveclem3b  24602  ovollb2  24663  ovolunlem1a  24670  ovolunlem1  24671  ovoliunlem1  24676  ovoliun2  24680  ioombl1lem4  24735  uniioombllem1  24755  uniioombllem2  24757  uniioombllem6  24762  mbfsup  24838  mbfinf  24839  mbflimsup  24840  itg1climres  24889  itg2monolem1  24925  itg2mono  24928  itg2i1fseq2  24931  itg2cnlem1  24936  minvecolem1  29244  rge0scvg  31907  esumpcvgval  32054  cvmsss2  33244  fin2so  35772  ptrecube  35785  heicant  35820  isbnd3  35950  totbndbnd  35955  rnnonrel  41180  stoweidlem35  43557  hoicvr  44067