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

Theorem dm0rn0 5263
Description: An empty domain implies 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 1697 . . . . . 6 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥𝑦 𝑥𝐴𝑦)
2 excom 2029 . . . . . 6 (∃𝑥𝑦 𝑥𝐴𝑦 ↔ ∃𝑦𝑥 𝑥𝐴𝑦)
31, 2xchbinx 323 . . . . 5 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦𝑥 𝑥𝐴𝑦)
4 alnex 1697 . . . . 5 (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦𝑥 𝑥𝐴𝑦)
53, 4bitr4i 266 . . . 4 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦)
6 noel 3878 . . . . . 6 ¬ 𝑥 ∈ ∅
76nbn 361 . . . . 5 (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
87albii 1737 . . . 4 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
9 noel 3878 . . . . . 6 ¬ 𝑦 ∈ ∅
109nbn 361 . . . . 5 (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
1110albii 1737 . . . 4 (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
125, 8, 113bitr3i 289 . . 3 (∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
13 abeq1 2720 . . 3 ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
14 abeq1 2720 . . 3 ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
1512, 13, 143bitr4i 291 . 2 ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
16 df-dm 5048 . . 3 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
1716eqeq1i 2615 . 2 (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
18 dfrn2 5233 . . 3 ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
1918eqeq1i 2615 . 2 (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
2015, 17, 193bitr4i 291 1 (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 195  wal 1473   = wceq 1475  wex 1695  wcel 1977  {cab 2596  c0 3874   class class class wbr 4583  dom cdm 5038  ran crn 5039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049
This theorem is referenced by:  rn0  5298  relrn0  5304  imadisj  5403  rnsnn0  5519  f00  6000  f0rn0  6003  2nd0  7066  iinon  7324  onoviun  7327  onnseq  7328  map0b  7782  fodomfib  8125  intrnfi  8205  wdomtr  8363  noinfep  8440  wemapwe  8477  fin23lem31  9048  fin23lem40  9056  isf34lem7  9084  isf34lem6  9085  ttukeylem6  9219  fodomb  9229  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  fseqsupcl  12638  fseqsupubi  12639  dmtrclfv  13607  ruclem11  14808  prmreclem6  15463  0ram  15562  0ram2  15563  0ramcl  15565  gsumval2  17103  ghmrn  17496  gexex  18079  gsumval3  18131  iinopn  20532  hauscmplem  21019  fbasrn  21498  alexsublem  21658  evth  22566  minveclem1  23003  minveclem3b  23007  ovollb2  23064  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliun2  23081  ioombl1lem4  23136  uniioombllem1  23155  uniioombllem2  23157  uniioombllem6  23162  mbfsup  23237  mbfinf  23238  mbflimsup  23239  itg1climres  23287  itg2monolem1  23323  itg2mono  23326  itg2i1fseq2  23329  itg2cnlem1  23334  minvecolem1  27114  rge0scvg  29323  esumpcvgval  29467  cvmsss2  30510  fin2so  32566  ptrecube  32579  heicant  32614  isbnd3  32753  totbndbnd  32758  rnnonrel  36916  rnmpt0  38407  stoweidlem35  38928  hoicvr  39438
  Copyright terms: Public domain W3C validator