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

Theorem imass2 5219
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 5146 . . 3  |-  ( A 
C_  B  ->  ( C  |`  A )  C_  ( C  |`  B ) )
2 rnss 5078 . . 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 4862 . 2  |-  ( C
" A )  =  ran  ( C  |`  A )
5 df-ima 4862 . 2  |-  ( C
" B )  =  ran  ( C  |`  B )
63, 4, 53sstr4g 3505 1  |-  ( A 
C_  B  ->  ( C " A )  C_  ( C " B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3436   ran crn 4850    |` cres 4851   "cima 4852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-xp 4855  df-cnv 4857  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862
This theorem is referenced by:  funimass1  5670  funimass2  5671  fvimacnv  6008  f1imass  6176  ecinxp  7442  sbthlem1  7684  sbthlem2  7685  php3  7760  ordtypelem2  8036  tcrank  8356  limsupgord  13513  isercoll  13716  isacs1i  15548  gsumzf1o  17531  dprdres  17646  dprd2da  17660  dmdprdsplit2lem  17663  lmhmlsp  18257  f1lindf  19364  iscnp4  20263  cnpco  20267  cncls2i  20270  cnntri  20271  cnrest2  20286  cnpresti  20288  cnprest  20289  1stcfb  20444  xkococnlem  20658  qtopval2  20695  tgqtop  20711  qtoprest  20716  kqdisj  20731  regr1lem  20738  kqreglem1  20740  kqreglem2  20741  kqnrmlem1  20742  kqnrmlem2  20743  nrmhmph  20793  fbasrn  20883  elfm2  20947  fmfnfmlem1  20953  fmco  20960  flffbas  20994  cnpflf2  20999  cnextcn  21066  metcnp3  21539  metustto  21552  cfilucfil  21558  uniioombllem3  22527  dyadmbllem  22541  mbfconstlem  22569  i1fima2  22621  itg2gt0  22702  ellimc3  22818  limcflf  22820  limcresi  22824  limciun  22833  lhop  22952  ig1peu  23106  ig1peuOLD  23107  ig1pdvds  23112  ig1pdvdsOLD  23118  psercnlem2  23363  dvloglem  23577  efopn  23587  txomap  28654  tpr2rico  28711  cvmsss2  29990  cvmopnlem  29994  cvmliftmolem1  29997  cvmliftlem15  30014  cvmlift2lem9  30027  nofulllem3  30583  imadifss  31839  poimirlem1  31852  poimirlem2  31853  poimirlem3  31854  poimirlem15  31866  poimirlem30  31881  dvtan  31903  heibor1lem  32052  isnumbasabl  35882  isnumbasgrp  35883  dfacbasgrp  35884  trclimalb2  36175  frege81d  36196  limccog  37517
  Copyright terms: Public domain W3C validator