Theorem imadisj 6064

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

Step	Hyp	Ref	Expression
1		df-ima 5656	. . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)
2	1	eqeq1i 2766	. 2 ⊢ ((𝐴 “ 𝐵) = ∅ ↔ ran (𝐴 ↾ 𝐵) = ∅)
3		dm0rn0 5896	. 2 ⊢ (dom (𝐴 ↾ 𝐵) = ∅ ↔ ran (𝐴 ↾ 𝐵) = ∅)
4		dmres 5994	. . . 4 ⊢ dom (𝐴 ↾ 𝐵) = (𝐵 ∩ dom 𝐴)
5		incom 4159	. . . 4 ⊢ (𝐵 ∩ dom 𝐴) = (dom 𝐴 ∩ 𝐵)
6	4, 5	eqtri 2784	. . 3 ⊢ dom (𝐴 ↾ 𝐵) = (dom 𝐴 ∩ 𝐵)
7	6	eqeq1i 2766	. 2 ⊢ (dom (𝐴 ↾ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅)
8	2, 3, 7	3bitr2i 301	1 ⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅)

Syntax hints:   ↔ wb 208   = wceq 1559   ∩ cin 3901  ∅c0 4283  dom cdm 5643  ran crn 5644   ↾ cres 5645   “ cima 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5649  df-cnv 5651  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656

This theorem is referenced by:  imadisjlnd  6065  ndmima  6087  fnimadisj  6647  fnimaeq0  6648  fimacnvdisj  6736  frxp2  8117  frxp3  8124  acndom2  10003  isf34lem5  10328  isf34lem7  10329  isf34lem6  10330  limsupgre  15498  isercolllem3  15684  pf1rcl  22399  cnconn  23469  1stcfb  23492  xkohaus  23700  qtopeu  23763  fbasrn  23931  mbflimsup  25715  preiman0  32872  eulerpartlemt  34628  erdszelem5  35505  fnwe2lem2  43588  imadisjld  44696