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

Theorem imass2 5023
Description: Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
imass2  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )

Proof of Theorem imass2
StepHypRef Expression
1 ssres2 4956 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 4881 . . 3  |-  ( ( C  |`  A )  C_  ( C  |`  B )  ->  ran  (  C  |`  A )  C_  ran  (  C  |`  B ) )
31, 2syl 17 . 2  |-  ( A 
C_  B  ->  ran  (  C  |`  A ) 
C_  ran  (  C  |`  B ) )
4 df-ima 4668 . 2  |-  ( C
" A )  =  ran  (  C  |`  A )
5 df-ima 4668 . 2  |-  ( C
" B )  =  ran  (  C  |`  B )
63, 4, 53sstr4g 3180 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    C_ wss 3113   ran crn 4648    |` cres 4649   "cima 4650
This theorem is referenced by:  funimass1  5249  funimass2  5250  fvimacnv  5560  f1imass  5708  ecinxp  6688  sbthlem1  6925  sbthlem2  6926  php3  7001  ordtypelem2  7188  mapfien  7353  tcrank  7508  limsupgord  11897  isercoll  12092  isacs1i  13507  gsumzf1o  15144  dprdres  15211  dprd2da  15225  dmdprdsplit2lem  15228  lmhmlsp  15754  cnpco  16944  cncls2i  16947  cnntri  16948  cnrest2  16962  cnpresti  16964  cnprest  16965  1stcfb  17119  xkococnlem  17301  qtopval2  17335  tgqtop  17351  qtoprest  17356  kqdisj  17371  regr1lem  17378  kqreglem1  17380  kqreglem2  17381  kqnrmlem1  17382  kqnrmlem2  17383  nrmhmph  17433  fbasrn  17527  elfm2  17591  fmfnfmlem1  17597  fmco  17604  flffbas  17638  cnpflf2  17643  metcnp3  18034  uniioombllem3  18888  dyadmbllem  18902  mbfconstlem  18932  i1fima2  18982  itg2gt0  19063  ellimc3  19177  limcflf  19179  limcresi  19183  limciun  19192  lhop  19311  ig1peu  19505  ig1pdvds  19510  psercnlem2  19748  dvloglem  19943  efopn  19953  cvmsss2  23163  cvmopnlem  23167  cvmliftmolem1  23170  cvmliftlem15  23187  cvmlift2lem9  23200  axfelem13  23713  prjpacp1  24480  prjpacp2  24481  iscnp4  24916  limptlimpr2lem2  24928  lvsovso  24979  heibor1lem  25886  isnumbasabl  26624  isnumbasgrp  26625  dfacbasgrp  26626  f1lindf  26645
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-br 3984  df-opab 4038  df-xp 4661  df-cnv 4663  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668
  Copyright terms: Public domain W3C validator