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

Theorem dm0rn0 5633
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 1744 . . . . . 6 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑥𝑦 𝑥𝐴𝑦)
2 excom 2096 . . . . . 6 (∃𝑥𝑦 𝑥𝐴𝑦 ↔ ∃𝑦𝑥 𝑥𝐴𝑦)
31, 2xchbinx 326 . . . . 5 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ¬ ∃𝑦𝑥 𝑥𝐴𝑦)
4 alnex 1744 . . . . 5 (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ¬ ∃𝑦𝑥 𝑥𝐴𝑦)
53, 4bitr4i 270 . . . 4 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦)
6 noel 4178 . . . . . 6 ¬ 𝑥 ∈ ∅
76nbn 365 . . . . 5 (¬ ∃𝑦 𝑥𝐴𝑦 ↔ (∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
87albii 1782 . . . 4 (∀𝑥 ¬ ∃𝑦 𝑥𝐴𝑦 ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
9 noel 4178 . . . . . 6 ¬ 𝑦 ∈ ∅
109nbn 365 . . . . 5 (¬ ∃𝑥 𝑥𝐴𝑦 ↔ (∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
1110albii 1782 . . . 4 (∀𝑦 ¬ ∃𝑥 𝑥𝐴𝑦 ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
125, 8, 113bitr3i 293 . . 3 (∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅) ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
13 abeq1 2892 . . 3 ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ ∀𝑥(∃𝑦 𝑥𝐴𝑦𝑥 ∈ ∅))
14 abeq1 2892 . . 3 ({𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅ ↔ ∀𝑦(∃𝑥 𝑥𝐴𝑦𝑦 ∈ ∅))
1512, 13, 143bitr4i 295 . 2 ({𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
16 df-dm 5410 . . 3 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
1716eqeq1i 2777 . 2 (dom 𝐴 = ∅ ↔ {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} = ∅)
18 dfrn2 5602 . . 3 ran 𝐴 = {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦}
1918eqeq1i 2777 . 2 (ran 𝐴 = ∅ ↔ {𝑦 ∣ ∃𝑥 𝑥𝐴𝑦} = ∅)
2015, 17, 193bitr4i 295 1 (dom 𝐴 = ∅ ↔ ran 𝐴 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wal 1505   = wceq 1507  wex 1742  wcel 2048  {cab 2753  c0 4173   class class class wbr 4923  dom cdm 5400  ran crn 5401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pr 5180
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924  df-opab 4986  df-cnv 5408  df-dm 5410  df-rn 5411
This theorem is referenced by:  rn0  5669  relrn0  5675  imadisj  5782  rnsnn0  5898  f00  6384  f0rn0  6387  2nd0  7501  iinon  7774  onoviun  7777  onnseq  7778  map0b  8238  fodomfib  8585  intrnfi  8667  wdomtr  8826  noinfep  8909  wemapwe  8946  fin23lem31  9555  fin23lem40  9563  isf34lem7  9591  isf34lem6  9592  ttukeylem6  9726  fodomb  9738  rpnnen1lem4  12187  rpnnen1lem5  12188  fseqsupcl  13153  fseqsupubi  13154  dmtrclfv  14229  ruclem11  15443  prmreclem6  16103  0ram  16202  0ram2  16203  0ramcl  16205  gsumval2  17738  ghmrn  18132  gexex  18719  gsumval3  18771  subdrgint  19294  iinopn  21204  hauscmplem  21708  fbasrn  22186  alexsublem  22346  evth  23256  minveclem1  23720  minveclem3b  23724  ovollb2  23783  ovolunlem1a  23790  ovolunlem1  23791  ovoliunlem1  23796  ovoliun2  23800  ioombl1lem4  23855  uniioombllem1  23875  uniioombllem2  23877  uniioombllem6  23882  mbfsup  23958  mbfinf  23959  mbflimsup  23960  itg1climres  24008  itg2monolem1  24044  itg2mono  24047  itg2i1fseq2  24050  itg2cnlem1  24055  minvecolem1  28419  rge0scvg  30793  esumpcvgval  30938  cvmsss2  32066  fin2so  34268  ptrecube  34281  heicant  34316  isbnd3  34452  totbndbnd  34457  rnnonrel  39258  rnmpt0  40854  stoweidlem35  41697  hoicvr  42207
  Copyright terms: Public domain W3C validator