Theorem imaco 5449

Description: Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.)

Assertion

Ref	Expression
imaco	|- ( ( A o. B ) " C ) = ( A " ( B " C ) )

Proof of Theorem imaco

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rex 2759	. . 3 |- ( E. y e. ( B " C ) y A x <-> E. y ( y e. ( B " C ) /\ y A x ) )
2		vex 3061	. . . 4 |- x e. _V
3	2	elima 5283	. . 3 |- ( x e. ( A " ( B " C ) ) <-> E. y e. ( B " C ) y A x )
4		rexcom4 3078	. . . . 5 |- ( E. z e. C E. y ( z B y /\ y A x ) <-> E. y E. z e. C ( z B y /\ y A x ) )
5		r19.41v 2958	. . . . . 6 |- ( E. z e. C ( z B y /\ y A x ) <-> ( E. z e. C z B y /\ y A x ) )
6	5	exbii 1688	. . . . 5 |- ( E. y E. z e. C ( z B y /\ y A x ) <-> E. y ( E. z e. C z B y /\ y A x ) )
7	4, 6	bitri 249	. . . 4 |- ( E. z e. C E. y ( z B y /\ y A x ) <-> E. y ( E. z e. C z B y /\ y A x ) )
8	2	elima 5283	. . . . 5 |- ( x e. ( ( A o. B ) " C ) <-> E. z e. C z ( A o. B ) x )
9		vex 3061	. . . . . . 7 |- z e. _V
10	9, 2	brco 5115	. . . . . 6 |- ( z ( A o. B ) x <-> E. y ( z B y /\ y A x ) )
11	10	rexbii 2905	. . . . 5 |- ( E. z e. C z ( A o. B ) x <-> E. z e. C E. y ( z B y /\ y A x ) )
12	8, 11	bitri 249	. . . 4 |- ( x e. ( ( A o. B ) " C ) <-> E. z e. C E. y ( z B y /\ y A x ) )
13		vex 3061	. . . . . . 7 |- y e. _V
14	13	elima 5283	. . . . . 6 |- ( y e. ( B " C ) <-> E. z e. C z B y )
15	14	anbi1i 693	. . . . 5 |- ( ( y e. ( B " C ) /\ y A x ) <-> ( E. z e. C z B y /\ y A x ) )
16	15	exbii 1688	. . . 4 |- ( E. y ( y e. ( B " C ) /\ y A x ) <-> E. y ( E. z e. C z B y /\ y A x ) )
17	7, 12, 16	3bitr4i 277	. . 3 |- ( x e. ( ( A o. B ) " C ) <-> E. y ( y e. ( B " C ) /\ y A x ) )
18	1, 3, 17	3bitr4ri 278	. 2 |- ( x e. ( ( A o. B ) " C ) <-> x e. ( A " ( B " C ) ) )
19	18	eqriv 2398	1 |- ( ( A o. B ) " C ) = ( A " ( B " C ) )

Syntax hints:   /\ wa 367   = wceq 1405   E.wex 1633   e. wcel 1842   E.wrex 2754   class class class wbr 4394   "cima 4945   o. ccom 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-xp 4948  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955

This theorem is referenced by:  fvco2  5880  supp0cosupp0  6896  imacosupp  6897  fipreima  7780  fsuppcolem  7814  mapfienOLD  8090  psgnunilem1  16734  gsumval3OLD  17124  gsumzf1o  17133  gsumzf1oOLD  17136  dprdf1o  17291  frlmup3  19019  f1lindf  19041  lindfmm  19046  cnco  19952  cnpco  19953  ptrescn  20324  xkoco1cn  20342  xkoco2cn  20343  xkococnlem  20344  qtopcn  20399  fmco  20646  uniioombllem3  22178  cncombf  22249  deg1val  22680  deg1valOLD  22681  ofpreima  27830  mbfmco  28592  eulerpartlemmf  28700  erdsze2lem2  29382  cvmliftmolem1  29459  cvmlift2lem9a  29481  cvmlift2lem9  29489  mclsppslem  29676  cnambfre  31416  ftc1anclem3  31446  trclimalb2  35686  brtrclfv2  35687  frege97d  35712  frege109d  35717  frege131d  35724  extoimad  35973  imo72b2lem0  35974  imo72b2lem2  35976  imo72b2lem1  35980  imo72b2  35985  limccog  36976