MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dm0rn0 Structured version   Visualization version   GIF version

Theorem dm0rn0 5937
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.
StepHypRef Expression
1 alnex 1777 . . . . . 6 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥𝑦 𝑥𝐴𝑦)
2 excom 2159 . . . . . 6 (∃𝑥𝑦 𝑥𝐴𝑦 ↔ ∃𝑦𝑥 𝑥𝐴𝑦)
31, 2xchbinx 334 . . . . 5 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦𝑥 𝑥𝐴𝑦)
4 alnex 1777 . . . . 5 (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦𝑥 𝑥𝐴𝑦)
53, 4bitr4i 278 . . . 4 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦)
6 noel 4343 . . . . . 6 ¬ 𝑥 ∈ ∅
76nbn 372 . . . . 5 (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
87albii 1815 . . . 4 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
9 noel 4343 . . . . . 6 ¬ 𝑦 ∈ ∅
109nbn 372 . . . . 5 (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
1110albii 1815 . . . 4 (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
125, 8, 113bitr3i 301 . . 3 (∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
13 eqabcb 2880 . . 3 ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
14 eqabcb 2880 . . 3 ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
1512, 13, 143bitr4i 303 . 2 ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
16 df-dm 5698 . . 3 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
1716eqeq1i 2739 . 2 (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
18 dfrn2 5901 . . 3 ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
1918eqeq1i 2739 . 2 (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
2015, 17, 193bitr4i 303 1 (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wal 1534   = wceq 1536  wex 1775  wcel 2105  {cab 2711  c0 4338   class class class wbr 5147  dom cdm 5688  ran crn 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699
This theorem is referenced by:  rn0  5938  relrn0  5985  imadisj  6099  rnsnn0  6229  rnmpt0f  6264  f00  6790  f0rn0  6793  2nd0  8019  iinon  8378  onoviun  8381  onnseq  8382  map0b  8921  fodomfib  9366  fodomfibOLD  9368  intrnfi  9453  wdomtr  9612  noinfep  9697  wemapwe  9734  fin23lem31  10380  fin23lem40  10388  isf34lem7  10416  isf34lem6  10417  ttukeylem6  10551  fodomb  10563  rpnnen1lem4  13019  rpnnen1lem5  13020  fseqsupcl  14014  fseqsupubi  14015  dmtrclfv  15053  ruclem11  16272  prmreclem6  16954  0ram  17053  0ram2  17054  0ramcl  17056  gsumval2  18711  ghmrn  19259  gexex  19885  gsumval3  19939  subdrgint  20820  iinopn  22923  hauscmplem  23429  fbasrn  23907  alexsublem  24067  evth  25004  minveclem1  25471  minveclem3b  25475  ovollb2  25537  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliun2  25554  ioombl1lem4  25609  uniioombllem1  25629  uniioombllem2  25631  uniioombllem6  25636  mbfsup  25712  mbfinf  25713  mbflimsup  25714  itg1climres  25763  itg2monolem1  25799  itg2mono  25802  itg2i1fseq2  25805  itg2cnlem1  25810  minvecolem1  30902  rge0scvg  33909  esumpcvgval  34058  cvmsss2  35258  fin2so  37593  ptrecube  37606  heicant  37641  isbnd3  37770  totbndbnd  37775  rnnonrel  43580  stoweidlem35  45990  hoicvr  46503
  Copyright terms: Public domain W3C validator