Theorem imassrn 6072

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 1898	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4019	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6064	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5878	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3987	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

This proof depends on syntax axioms:   ∧ wa 400  ∃wex 1808   ∈ wcel 2142  {cab 2740   ⊆ wss 3904  ⟨cop 4594  ran crn 5661   “ cima 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-xp 5666  df-cnv 5668  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673

This theorem is used by:  0ima  6079  cnvimass  6083  fimass  6726  isofrlem  7338  isofr2  7342  f1opw2  7667  imaexg  7908  f1oweALT  7967  frxp  8120  frxp2  8138  frxp3  8145  smores2  8339  naddunif  8678  naddasslem1  8679  naddasslem2  8680  ecss  8744  fopwdom  9071  sbthlem2  9074  sbthlem3  9075  sbthlem5  9077  sbthlem6  9078  ssenen  9137  ssfiALT  9156  fiint  9284  f1opwfi  9311  marypha1lem  9391  unxpwdom2  9548  tz9.12lem1  9757  djuin  9911  acndom2  10045  dfac12lem2  10135  isf34lem5  10368  isf34lem7  10369  isf34lem6  10370  enfin1ai  10374  hsmexlem4  10419  hsmexlem5  10420  fpwwe2lem5  10626  fpwwe2lem8  10629  tskuni  10774  limsupgle  15535  limsupval2  15538  limsupgre  15539  isercolllem2  15724  isercoll  15726  unbenlem  16974  imasless  17600  isacs1i  17719  isacs4lem  18606  mgmhmima  18779  mhmima  18890  cntzmhm  19417  f1omvdconj  19522  gsumzaddlem  19997  dmdprdd  20077  dprdfeq0  20100  dprdres  20106  dprdss  20107  dprdz  20108  subgdmdprd  20112  dprd2dlem1  20119  dprd2da  20120  dmdprdsplit2lem  20123  lmhmlsp  21181  frlmsslsp  21957  lindff1  21981  lindfrn  21982  f1lindf  21983  lindfmm  21988  lsslindf  21991  cnclsi  23440  cnprest2  23458  paste  23462  cmpfi  23576  connima  23593  1stcfb  23613  1stckgenlem  23721  kgencn3  23726  xkoco1cn  23825  xkoco2cn  23826  xkococnlem  23827  qtopval2  23864  basqtop  23879  imastopn  23888  kqopn  23902  kqcld  23903  hmeontr  23937  hmeores  23939  hmphdis  23964  cmphaushmeo  23968  qtopf1  23984  uzfbas  24066  elfm  24115  elfm3  24118  rnelfm  24121  cnextcn  24235  tgpconncomp  24281  qustgpopn  24288  tsmsf1o  24313  ustimasn  24396  utopbas  24403  restutop  24405  tgqioo  24968  cnheiborlem  25124  bndth  25128  fmcfil  25442  ovoliunlem1  25672  volsup  25726  uniioombllem4  25756  uniioombllem5  25757  opnmblALT  25773  volsup2  25775  mbfimaopnlem  25825  mbflimsup  25836  itg2gt0  25930  c1liplem1  26166  dvcnvrelem2  26188  mdegleb  26232  mdeglt  26233  mdegldg  26234  mdegxrcl  26235  mdegcl  26237  ig1peu  26343  efifo  26723  dvlog  26827  efopnlem2  26833  efopn  26834  bdayimaon  27868  noetasuplem4  27911  noetainflem4  27915  nobdaymin  27957  nocvxminlem  27958  noeta2  27965  etaslts2  27998  cutbdaybnd2lim  28001  oldf  28041  lrrecfr  28147  negsunif  28259  negbdaylem  28260  bdayons  28480  zssno  28585  f1otrg  29231  axcontlem10  29334  htthlem  31280  shsss  31676  imaelshi  32421  pjimai  32539  gsummpt2co  33377  gsumpart  33392  elrgspnsubrunlem2  33577  lsmsnorb  33713  dimkerim  34026  sitgclbn  34742  sitgaddlemb  34747  eulerpartlemgvv  34775  eulerpartlemgf  34778  coinfliprv  34882  ballotlemsima  34915  ballotlemro  34922  onvf1odlem4  35598  erdsze2lem2  35704  mrsubrn  36013  msubrn  36029  tailf  36914  dissneqlem  38014  poimirlem1  38300  poimirlem2  38301  poimirlem3  38302  poimirlem11  38310  poimirlem12  38311  poimirlem15  38314  poimirlem16  38315  poimirlem19  38318  poimirlem30  38329  itg2addnclem2  38351  itg2gt0cn  38354  ftc1anclem7  38378  ftc1anc  38380  ismtyima  38482  ismtyres  38487  heibor1lem  38488  reheibor  38518  elrfirn  43454  isnacs2  43465  isnacs3  43469  fnwe2lem2  43806  lmhmfgima  43839  brtrclfv2  44481  xphe  44535  imo72b2lem2  44921  imo72b2lem1  44923  imo72b2  44926  limccog  46364  liminfval2  46510  imaf1homlem  49913  imaidfu  49916