Theorem imassrn 6042

Description: The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.)

Assertion

Ref	Expression
imassrn	⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Proof of Theorem imassrn

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		exsimpr 1869	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4030	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6034	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5853	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3998	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  {cab 2707   ⊆ wss 3914  ⟨cop 4595  ran crn 5639   “ cima 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  0ima  6049  cnvimass  6053  f1imadifssran  6602  fimass  6708  isofrlem  7315  isofr2  7319  f1opw2  7644  imaexg  7889  f1oweALT  7951  frxp  8105  frxp2  8123  frxp3  8130  smores2  8323  naddunif  8657  naddasslem1  8658  naddasslem2  8659  ecss  8722  fopwdom  9049  sbthlem2  9052  sbthlem3  9053  sbthlem5  9055  sbthlem6  9056  ssenen  9115  ssfiALT  9138  fiint  9277  fiintOLD  9278  f1opwfi  9307  marypha1lem  9384  unxpwdom2  9541  tz9.12lem1  9740  djuin  9871  acndom2  10007  dfac12lem2  10098  isf34lem5  10331  isf34lem7  10332  isf34lem6  10333  enfin1ai  10337  hsmexlem4  10382  hsmexlem5  10383  fpwwe2lem5  10588  fpwwe2lem8  10591  tskuni  10736  limsupgle  15443  limsupval2  15446  limsupgre  15447  isercolllem2  15632  isercoll  15634  unbenlem  16879  imasless  17503  isacs1i  17618  isacs4lem  18503  mgmhmima  18642  mhmima  18752  cntzmhm  19273  f1omvdconj  19376  gsumzaddlem  19851  dmdprdd  19931  dprdfeq0  19954  dprdres  19960  dprdss  19961  dprdz  19962  subgdmdprd  19966  dprd2dlem1  19973  dprd2da  19974  dmdprdsplit2lem  19977  lmhmlsp  20956  frlmsslsp  21705  lindff1  21729  lindfrn  21730  f1lindf  21731  lindfmm  21736  lsslindf  21739  cnclsi  23159  cnprest2  23177  paste  23181  cmpfi  23295  connima  23312  1stcfb  23332  1stckgenlem  23440  kgencn3  23445  xkoco1cn  23544  xkoco2cn  23545  xkococnlem  23546  qtopval2  23583  basqtop  23598  imastopn  23607  kqopn  23621  kqcld  23622  hmeontr  23656  hmeores  23658  hmphdis  23683  cmphaushmeo  23687  qtopf1  23703  uzfbas  23785  elfm  23834  elfm3  23837  rnelfm  23840  cnextcn  23954  tgpconncomp  24000  qustgpopn  24007  tsmsf1o  24032  ustimasn  24116  utopbas  24123  restutop  24125  tgqioo  24688  cnheiborlem  24853  bndth  24857  fmcfil  25172  ovoliunlem1  25403  volsup  25457  uniioombllem4  25487  uniioombllem5  25488  opnmblALT  25504  volsup2  25506  mbfimaopnlem  25556  mbflimsup  25567  itg2gt0  25661  c1liplem1  25901  dvcnvrelem2  25923  mdegleb  25969  mdeglt  25970  mdegldg  25971  mdegxrcl  25972  mdegcl  25974  ig1peu  26080  efifo  26456  dvlog  26560  efopnlem2  26566  efopn  26567  bdayimaon  27605  noetasuplem4  27648  noetainflem4  27652  nocvxminlem  27689  nocvxmin  27690  noeta2  27696  etasslt2  27726  scutbdaybnd2lim  27729  oldf  27765  lrrecfr  27850  negsunif  27961  negsbdaylem  27962  bdayon  28173  zssno  28269  zs12bday  28343  f1otrg  28798  axcontlem10  28900  htthlem  30846  shsss  31242  imaelshi  31987  pjimai  32105  gsummpt2co  32988  gsumpart  32997  elrgspnsubrunlem2  33199  lsmsnorb  33362  dimkerim  33623  sitgclbn  34334  sitgaddlemb  34339  eulerpartlemgvv  34367  eulerpartlemgf  34370  coinfliprv  34474  ballotlemsima  34507  ballotlemro  34514  onvf1odlem4  35093  erdsze2lem2  35191  mrsubrn  35500  msubrn  35516  tailf  36363  dissneqlem  37328  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem11  37625  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem19  37633  poimirlem30  37644  itg2addnclem2  37666  itg2gt0cn  37669  ftc1anclem7  37693  ftc1anc  37695  ismtyima  37797  ismtyres  37802  heibor1lem  37803  reheibor  37833  elrfirn  42683  isnacs2  42694  isnacs3  42698  fnwe2lem2  43040  lmhmfgima  43073  brtrclfv2  43716  xphe  43770  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  limccog  45618  liminfval2  45766  imaf1homlem  49096  imaidfu  49099