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

Theorem imadisj 5202
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 4862 . . 3  |-  ( A
" B )  =  ran  ( A  |`  B )
21eqeq1i 2429 . 2  |-  ( ( A " B )  =  (/)  <->  ran  ( A  |`  B )  =  (/) )
3 dm0rn0 5066 . 2  |-  ( dom  ( A  |`  B )  =  (/)  <->  ran  ( A  |`  B )  =  (/) )
4 dmres 5140 . . . 4  |-  dom  ( A  |`  B )  =  ( B  i^i  dom  A )
5 incom 3655 . . . 4  |-  ( B  i^i  dom  A )  =  ( dom  A  i^i  B )
64, 5eqtri 2451 . . 3  |-  dom  ( A  |`  B )  =  ( dom  A  i^i  B )
76eqeq1i 2429 . 2  |-  ( dom  ( A  |`  B )  =  (/)  <->  ( dom  A  i^i  B )  =  (/) )
82, 3, 73bitr2i 276 1  |-  ( ( A " B )  =  (/)  <->  ( dom  A  i^i  B )  =  (/) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    = wceq 1437    i^i cin 3435   (/)c0 3761   dom cdm 4849   ran crn 4850    |` cres 4851   "cima 4852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pr 4656
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-xp 4855  df-cnv 4857  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862
This theorem is referenced by:  ndmima  5220  fnimadisj  5710  fnimaeq0  5711  fimacnvdisj  5774  acndom2  8485  isf34lem5  8808  isf34lem7  8809  isf34lem6  8810  limsupgre  13527  limsupgreOLD  13528  isercolllem3  13715  pf1rcl  18922  cnconn  20421  1stcfb  20444  xkohaus  20652  qtopeu  20715  fbasrn  20883  mbflimsup  22607  mbflimsupOLD  22608  eulerpartlemt  29197  erdszelem5  29911  fnwe2lem2  35826  imadisjld  36453  imadisjlnd  36454  wnefimgd  36455
  Copyright terms: Public domain W3C validator