Theorem imaco 5343

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 2721	. . 3 |- ( E. y e. ( B " C ) y A x <-> E. y ( y e. ( B " C ) /\ y A x ) )
2		vex 2975	. . . 4 |- x e. _V
3	2	elima 5174	. . 3 |- ( x e. ( A " ( B " C ) ) <-> E. y e. ( B " C ) y A x )
4		rexcom4 2992	. . . . 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 2873	. . . . . 6 |- ( E. z e. C ( z B y /\ y A x ) <-> ( E. z e. C z B y /\ y A x ) )
6	5	exbii 1634	. . . . 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 5174	. . . . 5 |- ( x e. ( ( A o. B ) " C ) <-> E. z e. C z ( A o. B ) x )
9		vex 2975	. . . . . . 7 |- z e. _V
10	9, 2	brco 5010	. . . . . 6 |- ( z ( A o. B ) x <-> E. y ( z B y /\ y A x ) )
11	10	rexbii 2740	. . . . 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 2975	. . . . . . 7 |- y e. _V
14	13	elima 5174	. . . . . 6 |- ( y e. ( B " C ) <-> E. z e. C z B y )
15	14	anbi1i 695	. . . . 5 |- ( ( y e. ( B " C ) /\ y A x ) <-> ( E. z e. C z B y /\ y A x ) )
16	15	exbii 1634	. . . 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 2440	1 |- ( ( A o. B ) " C ) = ( A " ( B " C ) )

Syntax hints:   /\ wa 369   = wceq 1369   E.wex 1586   e. wcel 1756   E.wrex 2716   class class class wbr 4292   "cima 4843   o. ccom 4844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-xp 4846  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853

This theorem is referenced by:  fvco2  5766  supp0cosupp0  6728  imacosupp  6729  fipreima  7617  fsuppcolem  7650  mapfienOLD  7927  psgnunilem1  15999  gsumval3OLD  16382  gsumzf1o  16391  gsumzf1oOLD  16394  dprdf1o  16529  frlmup3  18228  f1lindf  18251  lindfmm  18256  cnco  18870  cnpco  18871  ptrescn  19212  xkoco1cn  19230  xkoco2cn  19231  xkococnlem  19232  qtopcn  19287  fmco  19534  uniioombllem3  21065  cncombf  21136  deg1val  21567  deg1valOLD  21568  ofpreima  25984  mbfmco  26679  eulerpartlemmf  26758  erdsze2lem2  27092  cvmliftmolem1  27170  cvmlift2lem9a  27192  cvmlift2lem9  27200  cnambfre  28440  ftc1anclem3  28469