Theorem imassrn 6089

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 4067	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6081	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5900	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 4035	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  {cab 2714   ⊆ wss 3951  ⟨cop 4632  ran crn 5686   “ cima 5688

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698

This theorem is referenced by:  0ima  6096  cnvimass  6100  f1imadifssran  6652  fimass  6756  isofrlem  7360  isofr2  7364  f1opw2  7688  imaexg  7935  f1oweALT  7997  frxp  8151  frxp2  8169  frxp3  8176  smores2  8394  naddunif  8731  naddasslem1  8732  naddasslem2  8733  ecss  8793  fopwdom  9120  sbthlem2  9124  sbthlem3  9125  sbthlem5  9127  sbthlem6  9128  ssenen  9191  ssfiALT  9214  fiint  9366  fiintOLD  9367  f1opwfi  9396  marypha1lem  9473  unxpwdom2  9628  tz9.12lem1  9827  djuin  9958  acndom2  10094  dfac12lem2  10185  isf34lem5  10418  isf34lem7  10419  isf34lem6  10420  enfin1ai  10424  hsmexlem4  10469  hsmexlem5  10470  fpwwe2lem5  10675  fpwwe2lem8  10678  tskuni  10823  limsupgle  15513  limsupval2  15516  limsupgre  15517  isercolllem2  15702  isercoll  15704  unbenlem  16946  imasless  17585  isacs1i  17700  isacs4lem  18589  mgmhmima  18728  mhmima  18838  cntzmhm  19359  f1omvdconj  19464  gsumzaddlem  19939  dmdprdd  20019  dprdfeq0  20042  dprdres  20048  dprdss  20049  dprdz  20050  subgdmdprd  20054  dprd2dlem1  20061  dprd2da  20062  dmdprdsplit2lem  20065  lmhmlsp  21048  frlmsslsp  21816  lindff1  21840  lindfrn  21841  f1lindf  21842  lindfmm  21847  lsslindf  21850  cnclsi  23280  cnprest2  23298  paste  23302  cmpfi  23416  connima  23433  1stcfb  23453  1stckgenlem  23561  kgencn3  23566  xkoco1cn  23665  xkoco2cn  23666  xkococnlem  23667  qtopval2  23704  basqtop  23719  imastopn  23728  kqopn  23742  kqcld  23743  hmeontr  23777  hmeores  23779  hmphdis  23804  cmphaushmeo  23808  qtopf1  23824  uzfbas  23906  elfm  23955  elfm3  23958  rnelfm  23961  cnextcn  24075  tgpconncomp  24121  qustgpopn  24128  tsmsf1o  24153  ustimasn  24237  utopbas  24244  restutop  24246  tgqioo  24821  cnheiborlem  24986  bndth  24990  fmcfil  25306  ovoliunlem1  25537  volsup  25591  uniioombllem4  25621  uniioombllem5  25622  opnmblALT  25638  volsup2  25640  mbfimaopnlem  25690  mbflimsup  25701  itg2gt0  25795  c1liplem1  26035  dvcnvrelem2  26057  mdegleb  26103  mdeglt  26104  mdegldg  26105  mdegxrcl  26106  mdegcl  26108  ig1peu  26214  efifo  26589  dvlog  26693  efopnlem2  26699  efopn  26700  bdayimaon  27738  noetasuplem4  27781  noetainflem4  27785  nocvxminlem  27822  nocvxmin  27823  noeta2  27829  etasslt2  27859  scutbdaybnd2lim  27862  oldf  27896  lrrecfr  27976  negsunif  28087  negsbdaylem  28088  zssno  28367  zs12bday  28424  f1otrg  28879  axcontlem10  28988  htthlem  30936  shsss  31332  imaelshi  32077  pjimai  32195  gsummpt2co  33051  gsumpart  33060  elrgspnsubrunlem2  33252  lsmsnorb  33419  dimkerim  33678  sitgclbn  34345  sitgaddlemb  34350  eulerpartlemgvv  34378  eulerpartlemgf  34381  coinfliprv  34485  ballotlemsima  34518  ballotlemro  34525  erdsze2lem2  35209  mrsubrn  35518  msubrn  35534  tailf  36376  dissneqlem  37341  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem11  37638  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem19  37646  poimirlem30  37657  itg2addnclem2  37679  itg2gt0cn  37682  ftc1anclem7  37706  ftc1anc  37708  ismtyima  37810  ismtyres  37815  heibor1lem  37816  reheibor  37846  imaexALTV  38331  elrfirn  42706  isnacs2  42717  isnacs3  42721  fnwe2lem2  43063  lmhmfgima  43096  brtrclfv2  43740  xphe  43794  imo72b2lem2  44180  imo72b2lem1  44182  imo72b2  44185  limccog  45635  liminfval2  45783