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

Theorem imaco 5215
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.
StepHypRef Expression
1 df-rex 2583 . . 3  |-  ( E. y  e.  ( B
" C ) y A x  <->  E. y
( y  e.  ( B " C )  /\  y A x ) )
2 vex 2825 . . . 4  |-  x  e. 
_V
32elima 5054 . . 3  |-  ( x  e.  ( A "
( B " C
) )  <->  E. y  e.  ( B " C
) y A x )
4 rexcom4 2841 . . . . 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 2727 . . . . . 6  |-  ( E. z  e.  C  ( z B y  /\  y A x )  <->  ( E. z  e.  C  z B y  /\  y A x ) )
65exbii 1573 . . . . 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 ) )
74, 6bitri 240 . . . 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 ) )
82elima 5054 . . . . 5  |-  ( x  e.  ( ( A  o.  B ) " C )  <->  E. z  e.  C  z ( A  o.  B )
x )
9 vex 2825 . . . . . . 7  |-  z  e. 
_V
109, 2brco 4889 . . . . . 6  |-  ( z ( A  o.  B
) x  <->  E. y
( z B y  /\  y A x ) )
1110rexbii 2602 . . . . 5  |-  ( E. z  e.  C  z ( A  o.  B
) x  <->  E. z  e.  C  E. y
( z B y  /\  y A x ) )
128, 11bitri 240 . . . 4  |-  ( x  e.  ( ( A  o.  B ) " C )  <->  E. z  e.  C  E. y
( z B y  /\  y A x ) )
13 vex 2825 . . . . . . 7  |-  y  e. 
_V
1413elima 5054 . . . . . 6  |-  ( y  e.  ( B " C )  <->  E. z  e.  C  z B
y )
1514anbi1i 676 . . . . 5  |-  ( ( y  e.  ( B
" C )  /\  y A x )  <->  ( E. z  e.  C  z B y  /\  y A x ) )
1615exbii 1573 . . . 4  |-  ( E. y ( y  e.  ( B " C
)  /\  y A x )  <->  E. y
( E. z  e.  C  z B y  /\  y A x ) )
177, 12, 163bitr4i 268 . . 3  |-  ( x  e.  ( ( A  o.  B ) " C )  <->  E. y
( y  e.  ( B " C )  /\  y A x ) )
181, 3, 173bitr4ri 269 . 2  |-  ( x  e.  ( ( A  o.  B ) " C )  <->  x  e.  ( A " ( B
" C ) ) )
1918eqriv 2313 1  |-  ( ( A  o.  B )
" C )  =  ( A " ( B " C ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1532    = wceq 1633    e. wcel 1701   E.wrex 2578   class class class wbr 4060   "cima 4729    o. ccom 4730
This theorem is referenced by:  fvco2  5632  suppfif1  7194  fipreima  7206  mapfien  7444  gsumval3  15240  gsumzf1o  15245  dprdf1o  15316  cnco  17051  cnpco  17052  ptrescn  17389  xkoco1cn  17407  xkoco2cn  17408  xkococnlem  17409  qtopcn  17461  fmco  17708  uniioombllem3  18993  cncombf  19066  deg1val  19535  mbfmco  23788  erdsze2lem2  24019  cvmliftmolem1  24096  cvmlift2lem9a  24118  cvmlift2lem9  24126  frlmup3  26400  f1lindf  26440  lindfmm  26445  psgnunilem1  26564
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-br 4061  df-opab 4115  df-xp 4732  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739
  Copyright terms: Public domain W3C validator