Theorem imassrn 6030

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 1870	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4018	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6022	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5838	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3985	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  {cab 2714   ⊆ wss 3901  ⟨cop 4586  ran crn 5625   “ cima 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  0ima  6037  cnvimass  6041  f1imadifssran  6578  fimass  6682  isofrlem  7286  isofr2  7290  f1opw2  7613  imaexg  7855  f1oweALT  7916  frxp  8068  frxp2  8086  frxp3  8093  smores2  8286  naddunif  8621  naddasslem1  8622  naddasslem2  8623  ecss  8686  fopwdom  9013  sbthlem2  9016  sbthlem3  9017  sbthlem5  9019  sbthlem6  9020  ssenen  9079  ssfiALT  9098  fiint  9227  f1opwfi  9256  marypha1lem  9336  unxpwdom2  9493  tz9.12lem1  9699  djuin  9830  acndom2  9964  dfac12lem2  10055  isf34lem5  10288  isf34lem7  10289  isf34lem6  10290  enfin1ai  10294  hsmexlem4  10339  hsmexlem5  10340  fpwwe2lem5  10546  fpwwe2lem8  10549  tskuni  10694  limsupgle  15400  limsupval2  15403  limsupgre  15404  isercolllem2  15589  isercoll  15591  unbenlem  16836  imasless  17461  isacs1i  17580  isacs4lem  18467  mgmhmima  18640  mhmima  18750  cntzmhm  19270  f1omvdconj  19375  gsumzaddlem  19850  dmdprdd  19930  dprdfeq0  19953  dprdres  19959  dprdss  19960  dprdz  19961  subgdmdprd  19965  dprd2dlem1  19972  dprd2da  19973  dmdprdsplit2lem  19976  lmhmlsp  21001  frlmsslsp  21751  lindff1  21775  lindfrn  21776  f1lindf  21777  lindfmm  21782  lsslindf  21785  cnclsi  23216  cnprest2  23234  paste  23238  cmpfi  23352  connima  23369  1stcfb  23389  1stckgenlem  23497  kgencn3  23502  xkoco1cn  23601  xkoco2cn  23602  xkococnlem  23603  qtopval2  23640  basqtop  23655  imastopn  23664  kqopn  23678  kqcld  23679  hmeontr  23713  hmeores  23715  hmphdis  23740  cmphaushmeo  23744  qtopf1  23760  uzfbas  23842  elfm  23891  elfm3  23894  rnelfm  23897  cnextcn  24011  tgpconncomp  24057  qustgpopn  24064  tsmsf1o  24089  ustimasn  24172  utopbas  24179  restutop  24181  tgqioo  24744  cnheiborlem  24909  bndth  24913  fmcfil  25228  ovoliunlem1  25459  volsup  25513  uniioombllem4  25543  uniioombllem5  25544  opnmblALT  25560  volsup2  25562  mbfimaopnlem  25612  mbflimsup  25623  itg2gt0  25717  c1liplem1  25957  dvcnvrelem2  25979  mdegleb  26025  mdeglt  26026  mdegldg  26027  mdegxrcl  26028  mdegcl  26030  ig1peu  26136  efifo  26512  dvlog  26616  efopnlem2  26622  efopn  26623  bdayimaon  27661  noetasuplem4  27704  noetainflem4  27708  nobdaymin  27749  nocvxminlem  27750  noeta2  27757  etaslts2  27790  cutbdaybnd2lim  27793  oldf  27833  lrrecfr  27939  negsunif  28051  negbdaylem  28052  bdayons  28272  zssno  28377  f1otrg  28943  axcontlem10  29046  htthlem  30992  shsss  31388  imaelshi  32133  pjimai  32251  gsummpt2co  33131  gsumpart  33146  elrgspnsubrunlem2  33330  lsmsnorb  33472  dimkerim  33784  sitgclbn  34500  sitgaddlemb  34505  eulerpartlemgvv  34533  eulerpartlemgf  34536  coinfliprv  34640  ballotlemsima  34673  ballotlemro  34680  onvf1odlem4  35300  erdsze2lem2  35398  mrsubrn  35707  msubrn  35723  tailf  36569  dissneqlem  37541  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem11  37828  poimirlem12  37829  poimirlem15  37832  poimirlem16  37833  poimirlem19  37836  poimirlem30  37847  itg2addnclem2  37869  itg2gt0cn  37872  ftc1anclem7  37896  ftc1anc  37898  ismtyima  38000  ismtyres  38005  heibor1lem  38006  reheibor  38036  elrfirn  42933  isnacs2  42944  isnacs3  42948  fnwe2lem2  43289  lmhmfgima  43322  brtrclfv2  43964  xphe  44018  imo72b2lem2  44404  imo72b2lem1  44406  imo72b2  44409  limccog  45862  liminfval2  46008  imaf1homlem  49348  imaidfu  49351