Theorem imassrn 5980

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 1872	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4000	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 5972	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5798	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3964	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 396  ∃wex 1782   ∈ wcel 2106  {cab 2715   ⊆ wss 3887  ⟨cop 4567  ran crn 5590   “ cima 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602

This theorem is referenced by:  0ima  5986  cnvimass  5989  fimass  6621  fimacnvOLD  6948  isofrlem  7211  isofr2  7215  f1opw2  7524  imaexg  7762  f1oweALT  7815  frxp  7967  smores2  8185  ecss  8544  fopwdom  8867  sbthlem2  8871  sbthlem3  8872  sbthlem5  8874  sbthlem6  8875  ssenen  8938  ssfiALT  8957  fiint  9091  f1opwfi  9123  marypha1lem  9192  unxpwdom2  9347  tz9.12lem1  9545  djuin  9676  acndom2  9810  dfac12lem2  9900  isf34lem5  10134  isf34lem7  10135  isf34lem6  10136  enfin1ai  10140  hsmexlem4  10185  hsmexlem5  10186  fpwwe2lem5  10391  fpwwe2lem8  10394  tskuni  10539  limsupgle  15186  limsupval2  15189  limsupgre  15190  isercolllem2  15377  isercoll  15379  unbenlem  16609  imasless  17251  isacs1i  17366  isacs4lem  18262  mhmima  18463  cntzmhm  18945  f1omvdconj  19054  gsumzaddlem  19522  dmdprdd  19602  dprdfeq0  19625  dprdres  19631  dprdss  19632  dprdz  19633  subgdmdprd  19637  dprd2dlem1  19644  dprd2da  19645  dmdprdsplit2lem  19648  lmhmlsp  20311  frlmsslsp  21003  lindff1  21027  lindfrn  21028  f1lindf  21029  lindfmm  21034  lsslindf  21037  cnclsi  22423  cnprest2  22441  paste  22445  cmpfi  22559  connima  22576  1stcfb  22596  1stckgenlem  22704  kgencn3  22709  xkoco1cn  22808  xkoco2cn  22809  xkococnlem  22810  qtopval2  22847  basqtop  22862  imastopn  22871  kqopn  22885  kqcld  22886  hmeontr  22920  hmeores  22922  hmphdis  22947  cmphaushmeo  22951  qtopf1  22967  uzfbas  23049  elfm  23098  elfm3  23101  rnelfm  23104  cnextcn  23218  tgpconncomp  23264  qustgpopn  23271  tsmsf1o  23296  ustimasn  23380  utopbas  23387  restutop  23389  tgqioo  23963  cnheiborlem  24117  bndth  24121  fmcfil  24436  ovoliunlem1  24666  volsup  24720  uniioombllem4  24750  uniioombllem5  24751  opnmblALT  24767  volsup2  24769  mbfimaopnlem  24819  mbflimsup  24830  itg2gt0  24925  c1liplem1  25160  dvcnvrelem2  25182  mdegleb  25229  mdeglt  25230  mdegldg  25231  mdegxrcl  25232  mdegcl  25234  ig1peu  25336  efifo  25703  dvlog  25806  efopnlem2  25812  efopn  25813  f1otrg  27232  axcontlem10  27341  htthlem  29279  shsss  29675  imaelshi  30420  pjimai  30538  gsummpt2co  31308  gsumpart  31315  lsmsnorb  31579  dimkerim  31708  sitgclbn  32310  sitgaddlemb  32315  eulerpartlemgvv  32343  eulerpartlemgf  32346  coinfliprv  32449  ballotlemsima  32482  ballotlemro  32489  erdsze2lem2  33166  mrsubrn  33475  msubrn  33491  frxp2  33791  frxp3  33797  bdayimaon  33896  noetasuplem4  33939  noetainflem4  33943  nocvxminlem  33972  nocvxmin  33973  noeta2  33979  etasslt2  34008  scutbdaybnd2lim  34011  oldf  34041  lrrecfr  34100  tailf  34564  dissneqlem  35511  poimirlem1  35778  poimirlem2  35779  poimirlem3  35780  poimirlem11  35788  poimirlem12  35789  poimirlem15  35792  poimirlem16  35793  poimirlem19  35796  poimirlem30  35807  itg2addnclem2  35829  itg2gt0cn  35832  ftc1anclem7  35856  ftc1anc  35858  ismtyima  35961  ismtyres  35966  heibor1lem  35967  reheibor  35997  imaexALTV  36465  elrfirn  40517  isnacs2  40528  isnacs3  40532  fnwe2lem2  40876  lmhmfgima  40909  brtrclfv2  41335  xphe  41389  imo72b2lem0  41776  imo72b2lem2  41778  imo72b2lem1  41780  imo72b2  41783  limccog  43161  liminfval2  43309  mgmhmima  45356