Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ima GIF version

Definition df-ima 4564
 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 4563) and range (df-rn 4562). For an alternate definition, see dfima2 4895. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
df-ima (𝐴𝐵) = ran (𝐴𝐵)

Detailed syntax breakdown of Definition df-ima
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cima 4554 . 2 class (𝐴𝐵)
41, 2cres 4553 . . 3 class (𝐴𝐵)
54crn 4552 . 2 class ran (𝐴𝐵)
63, 5wceq 1332 1 wff (𝐴𝐵) = ran (𝐴𝐵)
 Colors of variables: wff set class This definition is referenced by:  resima  4864  resima2  4865  imaeq1  4888  imaeq2  4889  dfima2  4895  nfima  4901  rnresi  4908  resiima  4909  ima0  4910  imadisj  4913  imass1  4926  imass2  4927  ndmima  4928  imaundi  4963  imaundir  4964  inimass  4967  rninxp  4994  imainrect  4996  xpima1  4997  xpima2m  4998  dfrn4  5011  imacnvcnv  5015  imadmres  5043  mptpreima  5044  rnco2  5058  funcnvres  5208  funimacnv  5211  funimaexg  5219  fnima  5253  fores  5366  f1ores  5394  f1orescnv  5395  foimacnv  5397  resdif  5401  funfvima  5661  resfunexgALT  6020  smores2  6203  sbthlemi4  6865  sbthlemi6  6867  sbthlemi8  6869  djuin  6966  djuun  6969  casedm  6988  eninl  6999  eninr  7000  djudm  7007  tgrest  12413  cnconst2  12477  hmeores  12559
 Copyright terms: Public domain W3C validator