Theorem imassrn 6058

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

Syntax hints:   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  {cab 2713   ⊆ wss 3926  ⟨cop 4607  ran crn 5655   “ cima 5657

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667

This theorem is referenced by:  0ima  6065  cnvimass  6069  f1imadifssran  6621  fimass  6725  isofrlem  7332  isofr2  7336  f1opw2  7660  imaexg  7907  f1oweALT  7969  frxp  8123  frxp2  8141  frxp3  8148  smores2  8366  naddunif  8703  naddasslem1  8704  naddasslem2  8705  ecss  8765  fopwdom  9092  sbthlem2  9096  sbthlem3  9097  sbthlem5  9099  sbthlem6  9100  ssenen  9163  ssfiALT  9186  fiint  9336  fiintOLD  9337  f1opwfi  9366  marypha1lem  9443  unxpwdom2  9600  tz9.12lem1  9799  djuin  9930  acndom2  10066  dfac12lem2  10157  isf34lem5  10390  isf34lem7  10391  isf34lem6  10392  enfin1ai  10396  hsmexlem4  10441  hsmexlem5  10442  fpwwe2lem5  10647  fpwwe2lem8  10650  tskuni  10795  limsupgle  15491  limsupval2  15494  limsupgre  15495  isercolllem2  15680  isercoll  15682  unbenlem  16926  imasless  17552  isacs1i  17667  isacs4lem  18552  mgmhmima  18691  mhmima  18801  cntzmhm  19322  f1omvdconj  19425  gsumzaddlem  19900  dmdprdd  19980  dprdfeq0  20003  dprdres  20009  dprdss  20010  dprdz  20011  subgdmdprd  20015  dprd2dlem1  20022  dprd2da  20023  dmdprdsplit2lem  20026  lmhmlsp  21005  frlmsslsp  21754  lindff1  21778  lindfrn  21779  f1lindf  21780  lindfmm  21785  lsslindf  21788  cnclsi  23208  cnprest2  23226  paste  23230  cmpfi  23344  connima  23361  1stcfb  23381  1stckgenlem  23489  kgencn3  23494  xkoco1cn  23593  xkoco2cn  23594  xkococnlem  23595  qtopval2  23632  basqtop  23647  imastopn  23656  kqopn  23670  kqcld  23671  hmeontr  23705  hmeores  23707  hmphdis  23732  cmphaushmeo  23736  qtopf1  23752  uzfbas  23834  elfm  23883  elfm3  23886  rnelfm  23889  cnextcn  24003  tgpconncomp  24049  qustgpopn  24056  tsmsf1o  24081  ustimasn  24165  utopbas  24172  restutop  24174  tgqioo  24737  cnheiborlem  24902  bndth  24906  fmcfil  25222  ovoliunlem1  25453  volsup  25507  uniioombllem4  25537  uniioombllem5  25538  opnmblALT  25554  volsup2  25556  mbfimaopnlem  25606  mbflimsup  25617  itg2gt0  25711  c1liplem1  25951  dvcnvrelem2  25973  mdegleb  26019  mdeglt  26020  mdegldg  26021  mdegxrcl  26022  mdegcl  26024  ig1peu  26130  efifo  26506  dvlog  26610  efopnlem2  26616  efopn  26617  bdayimaon  27655  noetasuplem4  27698  noetainflem4  27702  nocvxminlem  27739  nocvxmin  27740  noeta2  27746  etasslt2  27776  scutbdaybnd2lim  27779  oldf  27813  lrrecfr  27893  negsunif  28004  negsbdaylem  28005  zssno  28284  zs12bday  28341  f1otrg  28796  axcontlem10  28898  htthlem  30844  shsss  31240  imaelshi  31985  pjimai  32103  gsummpt2co  32988  gsumpart  32997  elrgspnsubrunlem2  33189  lsmsnorb  33352  dimkerim  33613  sitgclbn  34321  sitgaddlemb  34326  eulerpartlemgvv  34354  eulerpartlemgf  34357  coinfliprv  34461  ballotlemsima  34494  ballotlemro  34501  erdsze2lem2  35172  mrsubrn  35481  msubrn  35497  tailf  36339  dissneqlem  37304  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem11  37601  poimirlem12  37602  poimirlem15  37605  poimirlem16  37606  poimirlem19  37609  poimirlem30  37620  itg2addnclem2  37642  itg2gt0cn  37645  ftc1anclem7  37669  ftc1anc  37671  ismtyima  37773  ismtyres  37778  heibor1lem  37779  reheibor  37809  imaexALTV  38294  elrfirn  42665  isnacs2  42676  isnacs3  42680  fnwe2lem2  43022  lmhmfgima  43055  brtrclfv2  43698  xphe  43752  imo72b2lem2  44138  imo72b2lem1  44140  imo72b2  44143  limccog  45597  liminfval2  45745  imaf1homlem  49014  imaidfu  49017