Definition df-ima 4732

Description: Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = { <. 2 , 6 >., <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F " B ) = { 6 } . Contrast with restriction (df-res 4731) and range (df-rn 4730). For an alternate definition, see dfima2 5070. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
df-ima	|- ( A " B ) = ran ( A |` B )

Detailed syntax breakdown of Definition df-ima

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cima 4722	. 2 class ( A " B )
4	1, 2	cres 4721	. . 3 class ( A |` B )
5	4	crn 4720	. 2 class ran ( A |` B )
6	3, 5	wceq 1395	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  5038  resima2  5039  imaeq1  5063  imaeq2  5064  dfima2  5070  nfima  5076  mptima  5080  rnresi  5085  resiima  5086  ima0  5087  imadisj  5090  imass1  5103  imass2  5104  ndmima  5105  imaundi  5141  imaundir  5142  inimass  5145  rninxp  5172  imainrect  5174  xpima1  5175  xpima2m  5176  dfrn4  5189  imacnvcnv  5193  imadmres  5221  mptpreima  5222  rnco2  5236  funcnvres  5394  funimacnv  5397  funimaexg  5405  fnima  5442  fores  5560  f1ores  5589  f1orescnv  5590  foimacnv  5592  resdif  5596  funfvima  5875  resfunexgALT  6259  smores2  6446  sbthlemi4  7138  sbthlemi6  7140  sbthlemi8  7142  djuin  7242  djuun  7245  casedm  7264  eninl  7275  eninr  7276  djudm  7283  ghmima  13817  conjsubg  13829  rnrhmsubrg  14231  tgrest  14858  cnconst2  14922  hmeores  15004  fsumdvdsmul  15680