Theorem imass2 5377

Description: Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.)

Assertion

Ref	Expression
imass2

Proof of Theorem imass2

Step	Hyp	Ref	Expression
1		ssres2 5305	. . 3
2		rnss 5236	. . 3
3	1, 2	syl 16	. 2
4		df-ima 5017	. 2
5		df-ima 5017	. 2
6	3, 4, 5	3sstr4g 3544	1

Syntax hints:  ->wi 4  C_wss 3475  rancrn 5005  |`cres 5006  "cima 5007

This theorem is referenced by:  funimass1  5666  funimass2  5667  fvimacnv  6002  f1imass  6172  ecinxp  7405  sbthlem1  7647  sbthlem2  7648  php3  7723  ordtypelem2  7965  mapfienOLD  8159  tcrank  8323  limsupgord  13295  isercoll  13490  isacs1i  15054  gsumzf1o  16917  gsumzf1oOLD  16920  dprdres  17075  dprd2da  17091  dmdprdsplit2lem  17094  lmhmlsp  17695  f1lindf  18857  iscnp4  19764  cnpco  19768  cncls2i  19771  cnntri  19772  cnrest2  19787  cnpresti  19789  cnprest  19790  1stcfb  19946  xkococnlem  20160  qtopval2  20197  tgqtop  20213  qtoprest  20218  kqdisj  20233  regr1lem  20240  kqreglem1  20242  kqreglem2  20243  kqnrmlem1  20244  kqnrmlem2  20245  nrmhmph  20295  fbasrn  20385  elfm2  20449  fmfnfmlem1  20455  fmco  20462  flffbas  20496  cnpflf2  20501  cnextcn  20567  metcnp3  21043  metusttoOLD  21060  metustto  21061  cfilucfilOLD  21072  cfilucfil  21073  uniioombllem3  21994  dyadmbllem  22008  mbfconstlem  22036  i1fima2  22086  itg2gt0  22167  ellimc3  22283  limcflf  22285  limcresi  22289  limciun  22298  lhop  22417  ig1peu  22572  ig1pdvds  22577  psercnlem2  22819  dvloglem  23029  efopn  23039  txomap  27837  tpr2rico  27894  cvmsss2  28719  cvmopnlem  28723  cvmliftmolem1  28726  cvmliftlem15  28743  cvmlift2lem9  28756  nofulllem3  29464  dvtan  30065  heibor1lem  30305  isnumbasabl  31055  isnumbasgrp  31056  dfacbasgrp  31057  limccog  31626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-cnv 5012  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017