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

Theorem dm0rn0 5763
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 1783 . . . . . 6 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥𝑦 𝑥𝐴𝑦)
2 excom 2167 . . . . . 6 (∃𝑥𝑦 𝑥𝐴𝑦 ↔ ∃𝑦𝑥 𝑥𝐴𝑦)
31, 2xchbinx 337 . . . . 5 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦𝑥 𝑥𝐴𝑦)
4 alnex 1783 . . . . 5 (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦𝑥 𝑥𝐴𝑦)
53, 4bitr4i 281 . . . 4 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦)
6 noel 4250 . . . . . 6 ¬ 𝑥 ∈ ∅
76nbn 376 . . . . 5 (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
87albii 1821 . . . 4 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
9 noel 4250 . . . . . 6 ¬ 𝑦 ∈ ∅
109nbn 376 . . . . 5 (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
1110albii 1821 . . . 4 (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
125, 8, 113bitr3i 304 . . 3 (∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
13 abeq1 2926 . . 3 ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
14 abeq1 2926 . . 3 ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
1512, 13, 143bitr4i 306 . 2 ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
16 df-dm 5533 . . 3 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
1716eqeq1i 2806 . 2 (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
18 dfrn2 5727 . . 3 ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
1918eqeq1i 2806 . 2 (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
2015, 17, 193bitr4i 306 1 (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wal 1536   = wceq 1538  wex 1781  wcel 2112  {cab 2779  c0 4246   class class class wbr 5033  dom cdm 5523  ran crn 5524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-cnv 5531  df-dm 5533  df-rn 5534
This theorem is referenced by:  rn0  5764  relrn0  5809  imadisj  5919  rnsnn0  6036  f00  6539  f0rn0  6542  2nd0  7682  iinon  7964  onoviun  7967  onnseq  7968  map0b  8434  fodomfib  8786  intrnfi  8868  wdomtr  9027  noinfep  9111  wemapwe  9148  fin23lem31  9758  fin23lem40  9766  isf34lem7  9794  isf34lem6  9795  ttukeylem6  9929  fodomb  9941  rpnnen1lem4  12371  rpnnen1lem5  12372  fseqsupcl  13344  fseqsupubi  13345  dmtrclfv  14373  ruclem11  15588  prmreclem6  16250  0ram  16349  0ram2  16350  0ramcl  16352  gsumval2  17891  ghmrn  18366  gexex  18969  gsumval3  19023  subdrgint  19578  iinopn  21510  hauscmplem  22014  fbasrn  22492  alexsublem  22652  evth  23567  minveclem1  24031  minveclem3b  24035  ovollb2  24096  ovolunlem1a  24103  ovolunlem1  24104  ovoliunlem1  24109  ovoliun2  24113  ioombl1lem4  24168  uniioombllem1  24188  uniioombllem2  24190  uniioombllem6  24195  mbfsup  24271  mbfinf  24272  mbflimsup  24273  itg1climres  24321  itg2monolem1  24357  itg2mono  24360  itg2i1fseq2  24363  itg2cnlem1  24368  minvecolem1  28660  rge0scvg  31300  esumpcvgval  31445  cvmsss2  32629  fin2so  35037  ptrecube  35050  heicant  35085  isbnd3  35215  totbndbnd  35220  rnnonrel  40278  rnmpt0  41836  stoweidlem35  42664  hoicvr  43174
  Copyright terms: Public domain W3C validator