Theorem imassrn 6090

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 1866	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4076	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6082	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5902	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 4038	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1775   ∈ wcel 2105  {cab 2711   ⊆ wss 3962  ⟨cop 4636  ran crn 5689   “ cima 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701

This theorem is referenced by:  0ima  6097  cnvimass  6101  fimass  6756  isofrlem  7359  isofr2  7363  f1opw2  7687  imaexg  7935  f1oweALT  7995  frxp  8149  frxp2  8167  frxp3  8174  smores2  8392  naddunif  8729  naddasslem1  8730  naddasslem2  8731  ecss  8791  fopwdom  9118  sbthlem2  9122  sbthlem3  9123  sbthlem5  9125  sbthlem6  9126  ssenen  9189  ssfiALT  9212  fiint  9363  fiintOLD  9364  f1opwfi  9393  marypha1lem  9470  unxpwdom2  9625  tz9.12lem1  9824  djuin  9955  acndom2  10091  dfac12lem2  10182  isf34lem5  10415  isf34lem7  10416  isf34lem6  10417  enfin1ai  10421  hsmexlem4  10466  hsmexlem5  10467  fpwwe2lem5  10672  fpwwe2lem8  10675  tskuni  10820  limsupgle  15509  limsupval2  15512  limsupgre  15513  isercolllem2  15698  isercoll  15700  unbenlem  16941  imasless  17586  isacs1i  17701  isacs4lem  18601  mgmhmima  18740  mhmima  18850  cntzmhm  19371  f1omvdconj  19478  gsumzaddlem  19953  dmdprdd  20033  dprdfeq0  20056  dprdres  20062  dprdss  20063  dprdz  20064  subgdmdprd  20068  dprd2dlem1  20075  dprd2da  20076  dmdprdsplit2lem  20079  lmhmlsp  21065  frlmsslsp  21833  lindff1  21857  lindfrn  21858  f1lindf  21859  lindfmm  21864  lsslindf  21867  cnclsi  23295  cnprest2  23313  paste  23317  cmpfi  23431  connima  23448  1stcfb  23468  1stckgenlem  23576  kgencn3  23581  xkoco1cn  23680  xkoco2cn  23681  xkococnlem  23682  qtopval2  23719  basqtop  23734  imastopn  23743  kqopn  23757  kqcld  23758  hmeontr  23792  hmeores  23794  hmphdis  23819  cmphaushmeo  23823  qtopf1  23839  uzfbas  23921  elfm  23970  elfm3  23973  rnelfm  23976  cnextcn  24090  tgpconncomp  24136  qustgpopn  24143  tsmsf1o  24168  ustimasn  24252  utopbas  24259  restutop  24261  tgqioo  24835  cnheiborlem  24999  bndth  25003  fmcfil  25319  ovoliunlem1  25550  volsup  25604  uniioombllem4  25634  uniioombllem5  25635  opnmblALT  25651  volsup2  25653  mbfimaopnlem  25703  mbflimsup  25714  itg2gt0  25809  c1liplem1  26049  dvcnvrelem2  26071  mdegleb  26117  mdeglt  26118  mdegldg  26119  mdegxrcl  26120  mdegcl  26122  ig1peu  26228  efifo  26603  dvlog  26707  efopnlem2  26713  efopn  26714  bdayimaon  27752  noetasuplem4  27795  noetainflem4  27799  nocvxminlem  27836  nocvxmin  27837  noeta2  27843  etasslt2  27873  scutbdaybnd2lim  27876  oldf  27910  lrrecfr  27990  negsunif  28101  negsbdaylem  28102  zssno  28381  zs12bday  28438  f1otrg  28893  axcontlem10  29002  htthlem  30945  shsss  31341  imaelshi  32086  pjimai  32204  gsummpt2co  33033  gsumpart  33042  lsmsnorb  33398  dimkerim  33654  sitgclbn  34324  sitgaddlemb  34329  eulerpartlemgvv  34357  eulerpartlemgf  34360  coinfliprv  34463  ballotlemsima  34496  ballotlemro  34503  erdsze2lem2  35188  mrsubrn  35497  msubrn  35513  tailf  36357  dissneqlem  37322  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem11  37617  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem19  37625  poimirlem30  37636  itg2addnclem2  37658  itg2gt0cn  37661  ftc1anclem7  37685  ftc1anc  37687  ismtyima  37789  ismtyres  37794  heibor1lem  37795  reheibor  37825  imaexALTV  38311  elrfirn  42682  isnacs2  42693  isnacs3  42697  fnwe2lem2  43039  lmhmfgima  43072  brtrclfv2  43716  xphe  43770  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  limccog  45575  liminfval2  45723