Theorem dm0rn0 5949

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 1779	. . . . . 6 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥∃𝑦 𝑥𝐴𝑦)
2		excom 2163	. . . . . 6 ⊢ (∃𝑥∃𝑦 𝑥𝐴𝑦 ↔ ∃𝑦∃𝑥 𝑥𝐴𝑦)
3	1, 2	xchbinx 334	. . . . 5 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦)
4		alnex 1779	. . . . 5 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦∃𝑥 𝑥𝐴𝑦)
5	3, 4	bitr4i 278	. . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦)
6		noel 4360	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
7	6	nbn 372	. . . . 5 ⊢ (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
8	7	albii 1817	. . . 4 ⊢ (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
9		noel 4360	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
10	9	nbn 372	. . . . 5 ⊢ (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
11	10	albii 1817	. . . 4 ⊢ (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
12	5, 8, 11	3bitr3i 301	. . 3 ⊢ (∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
13		eqabcb 2886	. . 3 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦 ↔ 𝑥 ∈ ∅))
14		eqabcb 2886	. . 3 ⊢ ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦 ↔ 𝑦 ∈ ∅))
15	12, 13, 14	3bitr4i 303	. 2 ⊢ ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
16		df-dm 5710	. . 3 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
17	16	eqeq1i 2745	. 2 ⊢ (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
18		dfrn2 5913	. . 3 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
19	18	eqeq1i 2745	. 2 ⊢ (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
20	15, 17, 19	3bitr4i 303	1 ⊢ (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108  {cab 2717  ∅c0 4352   class class class wbr 5166  dom cdm 5700  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  rn0  5950  relrn0  5995  imadisj  6109  rnsnn0  6239  rnmpt0f  6274  f00  6803  f0rn0  6806  2nd0  8037  iinon  8396  onoviun  8399  onnseq  8400  map0b  8941  fodomfib  9397  fodomfibOLD  9399  intrnfi  9485  wdomtr  9644  noinfep  9729  wemapwe  9766  fin23lem31  10412  fin23lem40  10420  isf34lem7  10448  isf34lem6  10449  ttukeylem6  10583  fodomb  10595  rpnnen1lem4  13045  rpnnen1lem5  13046  fseqsupcl  14028  fseqsupubi  14029  dmtrclfv  15067  ruclem11  16288  prmreclem6  16968  0ram  17067  0ram2  17068  0ramcl  17070  gsumval2  18724  ghmrn  19269  gexex  19895  gsumval3  19949  subdrgint  20826  iinopn  22929  hauscmplem  23435  fbasrn  23913  alexsublem  24073  evth  25010  minveclem1  25477  minveclem3b  25481  ovollb2  25543  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliun2  25560  ioombl1lem4  25615  uniioombllem1  25635  uniioombllem2  25637  uniioombllem6  25642  mbfsup  25718  mbfinf  25719  mbflimsup  25720  itg1climres  25769  itg2monolem1  25805  itg2mono  25808  itg2i1fseq2  25811  itg2cnlem1  25816  minvecolem1  30906  rge0scvg  33895  esumpcvgval  34042  cvmsss2  35242  fin2so  37567  ptrecube  37580  heicant  37615  isbnd3  37744  totbndbnd  37749  rnnonrel  43553  stoweidlem35  45956  hoicvr  46469