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

Theorem imadisj 6098
Description: A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.)
Assertion
Ref Expression
imadisj ((𝐴𝐵) = ∅ ↔ (dom 𝐴𝐵) = ∅)

Proof of Theorem imadisj
StepHypRef Expression
1 df-ima 5698 . . 3 (𝐴𝐵) = ran (𝐴𝐵)
21eqeq1i 2742 . 2 ((𝐴𝐵) = ∅ ↔ ran (𝐴𝐵) = ∅)
3 dm0rn0 5935 . 2 (dom (𝐴𝐵) = ∅ ↔ ran (𝐴𝐵) = ∅)
4 dmres 6030 . . . 4 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
5 incom 4209 . . . 4 (𝐵 ∩ dom 𝐴) = (dom 𝐴𝐵)
64, 5eqtri 2765 . . 3 dom (𝐴𝐵) = (dom 𝐴𝐵)
76eqeq1i 2742 . 2 (dom (𝐴𝐵) = ∅ ↔ (dom 𝐴𝐵) = ∅)
82, 3, 73bitr2i 299 1 ((𝐴𝐵) = ∅ ↔ (dom 𝐴𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  cin 3950  c0 4333  dom cdm 5685  ran crn 5686  cres 5687  cima 5688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698
This theorem is referenced by:  imadisjlnd  6099  ndmima  6121  fnimadisj  6700  fnimaeq0  6701  fimacnvdisj  6786  frxp2  8169  frxp3  8176  acndom2  10094  isf34lem5  10418  isf34lem7  10419  isf34lem6  10420  limsupgre  15517  isercolllem3  15703  pf1rcl  22353  cnconn  23430  1stcfb  23453  xkohaus  23661  qtopeu  23724  fbasrn  23892  mbflimsup  25701  preiman0  32719  eulerpartlemt  34373  erdszelem5  35200  fnwe2lem2  43063  imadisjld  44173
  Copyright terms: Public domain W3C validator