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

Theorem imaco 6250
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 3070 . . 3 (∃𝑦 ∈ (𝐵𝐶)𝑦𝐴𝑥 ↔ ∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥))
2 vex 3477 . . . 4 𝑥 ∈ V
32elima 6064 . . 3 (𝑥 ∈ (𝐴 “ (𝐵𝐶)) ↔ ∃𝑦 ∈ (𝐵𝐶)𝑦𝐴𝑥)
4 rexcom4 3284 . . . . 5 (∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥))
5 r19.41v 3187 . . . . . 6 (∃𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥) ↔ (∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
65exbii 1849 . . . . 5 (∃𝑦𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
74, 6bitri 275 . . . 4 (∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
82elima 6064 . . . . 5 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑧𝐶 𝑧(𝐴𝐵)𝑥)
9 vex 3477 . . . . . . 7 𝑧 ∈ V
109, 2brco 5870 . . . . . 6 (𝑧(𝐴𝐵)𝑥 ↔ ∃𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
1110rexbii 3093 . . . . 5 (∃𝑧𝐶 𝑧(𝐴𝐵)𝑥 ↔ ∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
128, 11bitri 275 . . . 4 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
13 vex 3477 . . . . . . 7 𝑦 ∈ V
1413elima 6064 . . . . . 6 (𝑦 ∈ (𝐵𝐶) ↔ ∃𝑧𝐶 𝑧𝐵𝑦)
1514anbi1i 623 . . . . 5 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥) ↔ (∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
1615exbii 1849 . . . 4 (∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
177, 12, 163bitr4i 303 . . 3 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥))
181, 3, 173bitr4ri 304 . 2 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ 𝑥 ∈ (𝐴 “ (𝐵𝐶)))
1918eqriv 2728 1 ((𝐴𝐵) “ 𝐶) = (𝐴 “ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1540  wex 1780  wcel 2105  wrex 3069   class class class wbr 5148  cima 5679  ccom 5680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-11 2153  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689
This theorem is referenced by:  fvco2  6988  suppco  8197  fipreima  9364  fsuppcolem  9402  psgnunilem1  19409  gsumzf1o  19828  dprdf1o  19950  frlmup3  21665  f1lindf  21687  lindfmm  21692  cnco  23090  cnpco  23091  ptrescn  23463  xkoco1cn  23481  xkoco2cn  23482  xkococnlem  23483  qtopcn  23538  fmco  23785  uniioombllem3  25434  cncombf  25507  deg1val  25952  ofpreima  32323  mbfmco  33727  eulerpartlemmf  33838  erdsze2lem2  34659  cvmliftmolem1  34736  cvmlift2lem9a  34758  cvmlift2lem9  34766  mclsppslem  35038  bj-imdirco  36535  poimirlem15  36967  poimirlem16  36968  poimirlem19  36971  cnambfre  37000  ftc1anclem3  37027  trclimalb2  42940  brtrclfv2  42941  frege97d  42966  frege109d  42971  frege131d  42978  extoimad  43379  imo72b2lem0  43380  imo72b2lem2  43382  imo72b2lem1  43384  imo72b2  43387  limccog  44795  smfco  45977  afv2co2  46424  isomgrtrlem  46965
  Copyright terms: Public domain W3C validator