Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imaco Structured version   Visualization version   GIF version

Theorem imaco 6082
 Description: Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.)
Assertion
Ref Expression
imaco ((𝐴𝐵) “ 𝐶) = (𝐴 “ (𝐵𝐶))

Proof of Theorem imaco
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rex 3136 . . 3 (∃𝑦 ∈ (𝐵𝐶)𝑦𝐴𝑥 ↔ ∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥))
2 vex 3472 . . . 4 𝑥 ∈ V
32elima 5912 . . 3 (𝑥 ∈ (𝐴 “ (𝐵𝐶)) ↔ ∃𝑦 ∈ (𝐵𝐶)𝑦𝐴𝑥)
4 rexcom4 3237 . . . . 5 (∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥))
5 r19.41v 3328 . . . . . 6 (∃𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥) ↔ (∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
65exbii 1849 . . . . 5 (∃𝑦𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
74, 6bitri 278 . . . 4 (∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
82elima 5912 . . . . 5 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑧𝐶 𝑧(𝐴𝐵)𝑥)
9 vex 3472 . . . . . . 7 𝑧 ∈ V
109, 2brco 5718 . . . . . 6 (𝑧(𝐴𝐵)𝑥 ↔ ∃𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
1110rexbii 3235 . . . . 5 (∃𝑧𝐶 𝑧(𝐴𝐵)𝑥 ↔ ∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
128, 11bitri 278 . . . 4 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
13 vex 3472 . . . . . . 7 𝑦 ∈ V
1413elima 5912 . . . . . 6 (𝑦 ∈ (𝐵𝐶) ↔ ∃𝑧𝐶 𝑧𝐵𝑦)
1514anbi1i 626 . . . . 5 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥) ↔ (∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
1615exbii 1849 . . . 4 (∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
177, 12, 163bitr4i 306 . . 3 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥))
181, 3, 173bitr4ri 307 . 2 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ 𝑥 ∈ (𝐴 “ (𝐵𝐶)))
1918eqriv 2819 1 ((𝐴𝐵) “ 𝐶) = (𝐴 “ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2114  ∃wrex 3131   class class class wbr 5042   “ cima 5535   ∘ ccom 5536 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-br 5043  df-opab 5105  df-xp 5538  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545 This theorem is referenced by:  fvco2  6740  suppco  7857  supp0cosupp0OLD  7860  imacosuppOLD  7862  fipreima  8818  fsuppcolem  8852  psgnunilem1  18612  gsumzf1o  19023  dprdf1o  19145  frlmup3  20487  f1lindf  20509  lindfmm  20514  cnco  21869  cnpco  21870  ptrescn  22242  xkoco1cn  22260  xkoco2cn  22261  xkococnlem  22262  qtopcn  22317  fmco  22564  uniioombllem3  24187  cncombf  24260  deg1val  24695  ofpreima  30418  mbfmco  31596  eulerpartlemmf  31707  erdsze2lem2  32525  cvmliftmolem1  32602  cvmlift2lem9a  32624  cvmlift2lem9  32632  mclsppslem  32904  bj-imdirco  34566  poimirlem15  35031  poimirlem16  35032  poimirlem19  35035  cnambfre  35064  ftc1anclem3  35091  trclimalb2  40358  brtrclfv2  40359  frege97d  40384  frege109d  40389  frege131d  40396  extoimad  40802  imo72b2lem0  40803  imo72b2lem2  40805  imo72b2lem1  40808  imo72b2  40812  limccog  42202  smfco  43374  afv2co2  43753  isomgrtrlem  44296
 Copyright terms: Public domain W3C validator