Theorem dm0rn0 5779

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 1789	. . . . . 6 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥∃𝑦 𝑥𝐴𝑦)
2		excom 2168	. . . . . 6 ⊢ (∃𝑥∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦∃𝑥 𝑥𝐴𝑦)
3	1, 2	xchbinx 337	. . . . 5 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦)
4		alnex 1789	. . . . 5 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦)
5	3, 4	bitr4i 281	. . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦)
6		noel 4231	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
7	6	nbn 376	. . . . 5 ⊢ (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
8	7	albii 1827	. . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
9		noel 4231	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
10	9	nbn 376	. . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
11	10	albii 1827	. . . 4 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
12	5, 8, 11	3bitr3i 304	. . 3 ⊢ (∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
13		abeq1 2863	. . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
14		abeq1 2863	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
15	12, 13, 14	3bitr4i 306	. 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
16		df-dm 5546	. . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
17	16	eqeq1i 2741	. 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
18		dfrn2 5742	. . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
19	18	eqeq1i 2741	. 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
20	15, 17, 19	3bitr4i 306	1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1541   = wceq 1543  ∃wex 1787   ∈ wcel 2112  {cab 2714  ∅c0 4223   class class class wbr 5039  dom cdm 5536  ran crn 5537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-cnv 5544  df-dm 5546  df-rn 5547

This theorem is referenced by:  rn0  5780  relrn0  5823  imadisj  5933  rnsnn0  6051  rnmpt0f  6086  f00  6579  f0rn0  6582  2nd0  7746  iinon  8055  onoviun  8058  onnseq  8059  map0b  8542  fodomfib  8928  intrnfi  9010  wdomtr  9169  noinfep  9253  wemapwe  9290  fin23lem31  9922  fin23lem40  9930  isf34lem7  9958  isf34lem6  9959  ttukeylem6  10093  fodomb  10105  rpnnen1lem4  12541  rpnnen1lem5  12542  fseqsupcl  13515  fseqsupubi  13516  dmtrclfv  14546  ruclem11  15764  prmreclem6  16437  0ram  16536  0ram2  16537  0ramcl  16539  gsumval2  18112  ghmrn  18589  gexex  19192  gsumval3  19246  subdrgint  19801  iinopn  21753  hauscmplem  22257  fbasrn  22735  alexsublem  22895  evth  23810  minveclem1  24275  minveclem3b  24279  ovollb2  24340  ovolunlem1a  24347  ovolunlem1  24348  ovoliunlem1  24353  ovoliun2  24357  ioombl1lem4  24412  uniioombllem1  24432  uniioombllem2  24434  uniioombllem6  24439  mbfsup  24515  mbfinf  24516  mbflimsup  24517  itg1climres  24566  itg2monolem1  24602  itg2mono  24605  itg2i1fseq2  24608  itg2cnlem1  24613  minvecolem1  28909  rge0scvg  31567  esumpcvgval  31712  cvmsss2  32903  fin2so  35450  ptrecube  35463  heicant  35498  isbnd3  35628  totbndbnd  35633  rnnonrel  40816  stoweidlem35  43194  hoicvr  43704