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

Theorem imadisj 5342
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  |-  ( ( A " B )  =  (/)  <->  ( dom  A  i^i  B )  =  (/) )

Proof of Theorem imadisj
StepHypRef Expression
1 df-ima 4998 . . 3  |-  ( A
" B )  =  ran  ( A  |`  B )
21eqeq1i 2448 . 2  |-  ( ( A " B )  =  (/)  <->  ran  ( A  |`  B )  =  (/) )
3 dm0rn0 5205 . 2  |-  ( dom  ( A  |`  B )  =  (/)  <->  ran  ( A  |`  B )  =  (/) )
4 dmres 5280 . . . 4  |-  dom  ( A  |`  B )  =  ( B  i^i  dom  A )
5 incom 3673 . . . 4  |-  ( B  i^i  dom  A )  =  ( dom  A  i^i  B )
64, 5eqtri 2470 . . 3  |-  dom  ( A  |`  B )  =  ( dom  A  i^i  B )
76eqeq1i 2448 . 2  |-  ( dom  ( A  |`  B )  =  (/)  <->  ( dom  A  i^i  B )  =  (/) )
82, 3, 73bitr2i 273 1  |-  ( ( A " B )  =  (/)  <->  ( dom  A  i^i  B )  =  (/) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1381    i^i cin 3457   (/)c0 3767   dom cdm 4985   ran crn 4986    |` cres 4987   "cima 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-br 4434  df-opab 4492  df-xp 4991  df-cnv 4993  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998
This theorem is referenced by:  fnimadisj  5687  fnimaeq0  5688  fimacnvdisj  5749  acndom2  8433  isf34lem5  8756  isf34lem7  8757  isf34lem6  8758  limsupgre  13278  isercolllem3  13463  pf1rcl  18253  cnconn  19789  1stcfb  19812  xkohaus  20020  qtopeu  20083  fbasrn  20251  mbflimsup  21939  eulerpartlemt  28176  erdszelem5  28505  fnwe2lem2  30965  imadisjld  37577  imadisjlnd  37578  wnefimgd  37579
  Copyright terms: Public domain W3C validator