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

Theorem imadisj 5163
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 4831 . . 3  |-  ( A
" B )  =  ran  ( A  |`  B )
21eqeq1i 2394 . 2  |-  ( ( A " B )  =  (/)  <->  ran  ( A  |`  B )  =  (/) )
3 dm0rn0 5026 . 2  |-  ( dom  ( A  |`  B )  =  (/)  <->  ran  ( A  |`  B )  =  (/) )
4 dmres 5107 . . . 4  |-  dom  ( A  |`  B )  =  ( B  i^i  dom  A )
5 incom 3476 . . . 4  |-  ( B  i^i  dom  A )  =  ( dom  A  i^i  B )
64, 5eqtri 2407 . . 3  |-  dom  ( A  |`  B )  =  ( dom  A  i^i  B )
76eqeq1i 2394 . 2  |-  ( dom  ( A  |`  B )  =  (/)  <->  ( dom  A  i^i  B )  =  (/) )
82, 3, 73bitr2i 265 1  |-  ( ( A " B )  =  (/)  <->  ( dom  A  i^i  B )  =  (/) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    i^i cin 3262   (/)c0 3571   dom cdm 4818   ran crn 4819    |` cres 4820   "cima 4821
This theorem is referenced by:  fnimadisj  5505  fnimaeq0  5506  fimacnvdisj  5561  acndom2  7868  isf34lem5  8191  isf34lem7  8192  isf34lem6  8193  limsupgre  12202  isercolllem3  12387  cnconn  17406  1stcfb  17429  xkohaus  17606  qtopeu  17669  fbasrn  17837  mbflimsup  19425  pf1rcl  19836  erdszelem5  24660  fnwe2lem2  26817
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-xp 4824  df-cnv 4826  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831
  Copyright terms: Public domain W3C validator