Theorem imassrn 6065

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 1902	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4014	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6057	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5871	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3982	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  {cab 2739   ⊆ wss 3899  ⟨cop 4590  ran crn 5652   “ cima 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  0ima  6072  cnvimass  6076  fimass  6722  isofrlem  7340  isofr2  7344  f1opw2  7668  imaexg  7914  f1oweALT  7973  frxp  8127  frxp2  8145  frxp3  8152  smores2  8346  naddunif  8687  naddasslem1  8688  naddasslem2  8689  ecss  8753  fopwdom  9088  sbthlem2  9091  sbthlem3  9092  sbthlem5  9094  sbthlem6  9095  ssenen  9154  ssfiALT  9173  fiint  9302  f1opwfi  9329  marypha1lem  9409  unxpwdom2  9566  tz9.12lem1  9777  djuin  9980  acndom2  10114  dfac12lem2  10204  isf34lem5  10437  isf34lem7  10438  isf34lem6  10439  enfin1ai  10443  hsmexlem4  10488  hsmexlem5  10489  fpwwe2lem5  10701  fpwwe2lem8  10704  tskuni  10849  limsupgle  15624  limsupval2  15627  limsupgre  15628  isercolllem2  15813  isercoll  15815  unbenlem  17066  imasless  17692  isacs1i  17811  isacs4lem  18698  mgmhmima  18884  mhmima  19001  cntzmhm  19535  f1omvdconj  19640  gsumzaddlem  20115  dmdprdd  20195  dprdfeq0  20218  dprdres  20224  dprdss  20225  dprdz  20226  subgdmdprd  20230  dprd2dlem1  20237  dprd2da  20238  dmdprdsplit2lem  20241  lmhmlsp  21304  frlmsslsp  22082  lindff1  22106  lindfrn  22107  f1lindf  22108  lindfmm  22113  lsslindf  22116  cnclsi  23570  cnprest2  23588  paste  23592  cmpfi  23706  connima  23723  1stcfb  23743  1stckgenlem  23852  kgencn3  23857  xkoco1cn  23956  xkoco2cn  23957  xkococnlem  23958  qtopval2  23995  basqtop  24010  imastopn  24019  kqopn  24033  kqcld  24034  hmeontr  24068  hmeores  24070  hmphdis  24095  cmphaushmeo  24099  qtopf1  24115  uzfbas  24197  elfm  24246  elfm3  24249  rnelfm  24252  cnextcn  24366  tgpconncomp  24412  qustgpopn  24419  tsmsf1o  24444  ustimasn  24527  utopbas  24534  restutop  24536  tgqioo  25099  cnheiborlem  25255  bndth  25259  fmcfil  25573  ovoliunlem1  25803  volsup  25857  uniioombllem4  25887  uniioombllem5  25888  opnmblALT  25904  volsup2  25906  mbfimaopnlem  25956  mbflimsup  25967  itg2gt0  26061  c1liplem1  26296  dvcnvrelem2  26318  mdegleb  26362  mdeglt  26363  mdegldg  26364  mdegxrcl  26365  mdegcl  26367  ig1peu  26473  efifo  26857  dvlog  26961  efopnlem2  26967  efopn  26968  bdayimaon  28032  noetasuplem4  28075  noetainflem4  28079  nobdaymin  28121  nocvxminlem  28122  noeta2  28129  etaslts2  28162  cutbdaybnd2lim  28165  oldf  28205  lrrecfr  28311  negsunif  28423  negbdaylem  28424  bdayons  28644  zssno  28749  cgrabasimass  29360  f1otrg  29430  axcontlem10  29533  htthlem  31501  shsss  31897  imaelshi  32642  pjimai  32760  gsummpt2co  33591  gsumpart  33606  elrgspnsubrunlem2  33791  lsmsnorb  33928  dimkerim  34241  sitgclbn  34958  sitgaddlemb  34963  eulerpartlemgvv  34991  eulerpartlemgf  34994  coinfliprv  35098  ballotlemsima  35131  ballotlemro  35138  onvf1odlem4  35858  erdsze2lem2  35938  mrsubrn  36247  msubrn  36263  tailf  37133  dissneqlem  38231  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem11  38517  poimirlem12  38518  poimirlem15  38521  poimirlem16  38522  poimirlem19  38525  poimirlem30  38536  itg2addnclem2  38558  itg2gt0cn  38561  ftc1anclem7  38585  ftc1anc  38587  ismtyima  38705  ismtyres  38710  heibor1lem  38711  reheibor  38741  elrfirn  43659  isnacs2  43670  isnacs3  43674  fnwe2lem2  44011  lmhmfgima  44044  brtrclfv2  44686  xphe  44740  imo72b2lem2  45126  imo72b2lem1  45128  imo72b2  45131  limccog  46576  liminfval2  46722  imaf1homlem  50159  imaidfu  50162