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

Theorem imaco 6273
Description: Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.) (Proof shortened by Wolf Lammen, 16-May-2025.)
Assertion
Ref Expression
imaco ((𝐴𝐵) “ 𝐶) = (𝐴 “ (𝐵𝐶))

Proof of Theorem imaco
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rex 3069 . . 3 (∃𝑦 ∈ (𝐵𝐶)𝑦𝐴𝑥 ↔ ∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥))
2 vex 3482 . . . 4 𝑥 ∈ V
32elima 6085 . . 3 (𝑥 ∈ (𝐴 “ (𝐵𝐶)) ↔ ∃𝑦 ∈ (𝐵𝐶)𝑦𝐴𝑥)
4 vex 3482 . . . . . . 7 𝑧 ∈ V
54, 2brco 5884 . . . . . 6 (𝑧(𝐴𝐵)𝑥 ↔ ∃𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
65rexbii 3092 . . . . 5 (∃𝑧𝐶 𝑧(𝐴𝐵)𝑥 ↔ ∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
7 rexcom4 3286 . . . . 5 (∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥))
8 r19.41v 3187 . . . . . 6 (∃𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥) ↔ (∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
98exbii 1845 . . . . 5 (∃𝑦𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
106, 7, 93bitri 297 . . . 4 (∃𝑧𝐶 𝑧(𝐴𝐵)𝑥 ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
112elima 6085 . . . 4 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑧𝐶 𝑧(𝐴𝐵)𝑥)
12 vex 3482 . . . . . . 7 𝑦 ∈ V
1312elima 6085 . . . . . 6 (𝑦 ∈ (𝐵𝐶) ↔ ∃𝑧𝐶 𝑧𝐵𝑦)
1413anbi1i 624 . . . . 5 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥) ↔ (∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
1514exbii 1845 . . . 4 (∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
1610, 11, 153bitr4i 303 . . 3 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥))
171, 3, 163bitr4ri 304 . 2 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ 𝑥 ∈ (𝐴 “ (𝐵𝐶)))
1817eqriv 2732 1 ((𝐴𝐵) “ 𝐶) = (𝐴 “ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1537  wex 1776  wcel 2106  wrex 3068   class class class wbr 5148  cima 5692  ccom 5693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-11 2155  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702
This theorem is referenced by:  fvco2  7006  suppco  8230  fipreima  9396  fsuppcolem  9439  psgnunilem1  19526  gsumzf1o  19945  dprdf1o  20067  frlmup3  21838  f1lindf  21860  lindfmm  21865  cnco  23290  cnpco  23291  ptrescn  23663  xkoco1cn  23681  xkoco2cn  23682  xkococnlem  23683  qtopcn  23738  fmco  23985  uniioombllem3  25634  cncombf  25707  deg1val  26150  ofpreima  32682  mbfmco  34246  eulerpartlemmf  34357  erdsze2lem2  35189  cvmliftmolem1  35266  cvmlift2lem9a  35288  cvmlift2lem9  35296  mclsppslem  35568  bj-imdirco  37173  poimirlem15  37622  poimirlem16  37623  poimirlem19  37626  cnambfre  37655  ftc1anclem3  37682  aks6d1c6lem4  42155  aks6d1c6lem5  42159  trclimalb2  43716  brtrclfv2  43717  frege97d  43742  frege109d  43747  frege131d  43754  extoimad  44154  imo72b2lem0  44155  imo72b2lem2  44157  imo72b2lem1  44159  imo72b2  44162  limccog  45576  smfco  46758  afv2co2  47207  grimco  47818
  Copyright terms: Public domain W3C validator