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

Theorem imaco 5599
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 2913 . . 3 (∃𝑦 ∈ (𝐵𝐶)𝑦𝐴𝑥 ↔ ∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥))
2 vex 3189 . . . 4 𝑥 ∈ V
32elima 5430 . . 3 (𝑥 ∈ (𝐴 “ (𝐵𝐶)) ↔ ∃𝑦 ∈ (𝐵𝐶)𝑦𝐴𝑥)
4 rexcom4 3211 . . . . 5 (∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥))
5 r19.41v 3081 . . . . . 6 (∃𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥) ↔ (∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
65exbii 1771 . . . . 5 (∃𝑦𝑧𝐶 (𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
74, 6bitri 264 . . . 4 (∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
82elima 5430 . . . . 5 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑧𝐶 𝑧(𝐴𝐵)𝑥)
9 vex 3189 . . . . . . 7 𝑧 ∈ V
109, 2brco 5252 . . . . . 6 (𝑧(𝐴𝐵)𝑥 ↔ ∃𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
1110rexbii 3034 . . . . 5 (∃𝑧𝐶 𝑧(𝐴𝐵)𝑥 ↔ ∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
128, 11bitri 264 . . . 4 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑧𝐶𝑦(𝑧𝐵𝑦𝑦𝐴𝑥))
13 vex 3189 . . . . . . 7 𝑦 ∈ V
1413elima 5430 . . . . . 6 (𝑦 ∈ (𝐵𝐶) ↔ ∃𝑧𝐶 𝑧𝐵𝑦)
1514anbi1i 730 . . . . 5 ((𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥) ↔ (∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
1615exbii 1771 . . . 4 (∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥) ↔ ∃𝑦(∃𝑧𝐶 𝑧𝐵𝑦𝑦𝐴𝑥))
177, 12, 163bitr4i 292 . . 3 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ ∃𝑦(𝑦 ∈ (𝐵𝐶) ∧ 𝑦𝐴𝑥))
181, 3, 173bitr4ri 293 . 2 (𝑥 ∈ ((𝐴𝐵) “ 𝐶) ↔ 𝑥 ∈ (𝐴 “ (𝐵𝐶)))
1918eqriv 2618 1 ((𝐴𝐵) “ 𝐶) = (𝐴 “ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1480  wex 1701  wcel 1987  wrex 2908   class class class wbr 4613  cima 5077  ccom 5078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-opab 4674  df-xp 5080  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087
This theorem is referenced by:  fvco2  6230  supp0cosupp0  7279  imacosupp  7280  fipreima  8216  fsuppcolem  8250  psgnunilem1  17834  gsumzf1o  18234  dprdf1o  18352  frlmup3  20058  f1lindf  20080  lindfmm  20085  cnco  20980  cnpco  20981  ptrescn  21352  xkoco1cn  21370  xkoco2cn  21371  xkococnlem  21372  qtopcn  21427  fmco  21675  uniioombllem3  23259  cncombf  23331  deg1val  23760  ofpreima  29308  mbfmco  30107  eulerpartlemmf  30218  erdsze2lem2  30894  cvmliftmolem1  30971  cvmlift2lem9a  30993  cvmlift2lem9  31001  mclsppslem  31188  poimirlem15  33056  poimirlem16  33057  poimirlem19  33060  cnambfre  33090  ftc1anclem3  33119  trclimalb2  37499  brtrclfv2  37500  frege97d  37525  frege109d  37530  frege131d  37537  extoimad  37946  imo72b2lem0  37947  imo72b2lem2  37949  imo72b2lem1  37953  imo72b2  37957  limccog  39256  smfco  40316
  Copyright terms: Public domain W3C validator