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

Theorem imadisj 5178
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 4842 . . 3  |-  ( A
" B )  =  ran  ( A  |`  B )
21eqeq1i 2442 . 2  |-  ( ( A " B )  =  (/)  <->  ran  ( A  |`  B )  =  (/) )
3 dm0rn0 5045 . 2  |-  ( dom  ( A  |`  B )  =  (/)  <->  ran  ( A  |`  B )  =  (/) )
4 dmres 5121 . . . 4  |-  dom  ( A  |`  B )  =  ( B  i^i  dom  A )
5 incom 3533 . . . 4  |-  ( B  i^i  dom  A )  =  ( dom  A  i^i  B )
64, 5eqtri 2455 . . 3  |-  dom  ( A  |`  B )  =  ( dom  A  i^i  B )
76eqeq1i 2442 . 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 1364    i^i cin 3317   (/)c0 3627   dom cdm 4829   ran crn 4830    |` cres 4831   "cima 4832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pr 4521
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2966  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-sn 3868  df-pr 3870  df-op 3874  df-br 4283  df-opab 4341  df-xp 4835  df-cnv 4837  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842
This theorem is referenced by:  fnimadisj  5521  fnimaeq0  5522  fimacnvdisj  5579  acndom2  8214  isf34lem5  8537  isf34lem7  8538  isf34lem6  8539  limsupgre  12945  isercolllem3  13130  cnconn  18870  1stcfb  18893  xkohaus  19070  qtopeu  19133  fbasrn  19301  mbflimsup  20988  pf1rcl  21402  eulerpartlemt  26604  erdszelem5  26933  fnwe2lem2  29251
  Copyright terms: Public domain W3C validator