Theorem imassrn 6038

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 1871	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4020	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6030	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5846	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3987	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  {cab 2715   ⊆ wss 3903  ⟨cop 4588  ran crn 5633   “ cima 5635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  0ima  6045  cnvimass  6049  f1imadifssran  6586  fimass  6690  isofrlem  7296  isofr2  7300  f1opw2  7623  imaexg  7865  f1oweALT  7926  frxp  8078  frxp2  8096  frxp3  8103  smores2  8296  naddunif  8631  naddasslem1  8632  naddasslem2  8633  ecss  8697  fopwdom  9025  sbthlem2  9028  sbthlem3  9029  sbthlem5  9031  sbthlem6  9032  ssenen  9091  ssfiALT  9110  fiint  9239  f1opwfi  9268  marypha1lem  9348  unxpwdom2  9505  tz9.12lem1  9711  djuin  9842  acndom2  9976  dfac12lem2  10067  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  enfin1ai  10306  hsmexlem4  10351  hsmexlem5  10352  fpwwe2lem5  10558  fpwwe2lem8  10561  tskuni  10706  limsupgle  15412  limsupval2  15415  limsupgre  15416  isercolllem2  15601  isercoll  15603  unbenlem  16848  imasless  17473  isacs1i  17592  isacs4lem  18479  mgmhmima  18652  mhmima  18762  cntzmhm  19282  f1omvdconj  19387  gsumzaddlem  19862  dmdprdd  19942  dprdfeq0  19965  dprdres  19971  dprdss  19972  dprdz  19973  subgdmdprd  19977  dprd2dlem1  19984  dprd2da  19985  dmdprdsplit2lem  19988  lmhmlsp  21013  frlmsslsp  21763  lindff1  21787  lindfrn  21788  f1lindf  21789  lindfmm  21794  lsslindf  21797  cnclsi  23228  cnprest2  23246  paste  23250  cmpfi  23364  connima  23381  1stcfb  23401  1stckgenlem  23509  kgencn3  23514  xkoco1cn  23613  xkoco2cn  23614  xkococnlem  23615  qtopval2  23652  basqtop  23667  imastopn  23676  kqopn  23690  kqcld  23691  hmeontr  23725  hmeores  23727  hmphdis  23752  cmphaushmeo  23756  qtopf1  23772  uzfbas  23854  elfm  23903  elfm3  23906  rnelfm  23909  cnextcn  24023  tgpconncomp  24069  qustgpopn  24076  tsmsf1o  24101  ustimasn  24184  utopbas  24191  restutop  24193  tgqioo  24756  cnheiborlem  24921  bndth  24925  fmcfil  25240  ovoliunlem1  25471  volsup  25525  uniioombllem4  25555  uniioombllem5  25556  opnmblALT  25572  volsup2  25574  mbfimaopnlem  25624  mbflimsup  25635  itg2gt0  25729  c1liplem1  25969  dvcnvrelem2  25991  mdegleb  26037  mdeglt  26038  mdegldg  26039  mdegxrcl  26040  mdegcl  26042  ig1peu  26148  efifo  26524  dvlog  26628  efopnlem2  26634  efopn  26635  bdayimaon  27673  noetasuplem4  27716  noetainflem4  27720  nobdaymin  27761  nocvxminlem  27762  noeta2  27769  etaslts2  27802  cutbdaybnd2lim  27805  oldf  27845  lrrecfr  27951  negsunif  28063  negbdaylem  28064  bdayons  28284  zssno  28389  f1otrg  28955  axcontlem10  29058  htthlem  31004  shsss  31400  imaelshi  32145  pjimai  32263  gsummpt2co  33141  gsumpart  33156  elrgspnsubrunlem2  33341  lsmsnorb  33483  dimkerim  33804  sitgclbn  34520  sitgaddlemb  34525  eulerpartlemgvv  34553  eulerpartlemgf  34556  coinfliprv  34660  ballotlemsima  34693  ballotlemro  34700  onvf1odlem4  35319  erdsze2lem2  35417  mrsubrn  35726  msubrn  35742  tailf  36588  dissneqlem  37589  poimirlem1  37866  poimirlem2  37867  poimirlem3  37868  poimirlem11  37876  poimirlem12  37877  poimirlem15  37880  poimirlem16  37881  poimirlem19  37884  poimirlem30  37895  itg2addnclem2  37917  itg2gt0cn  37920  ftc1anclem7  37944  ftc1anc  37946  ismtyima  38048  ismtyres  38053  heibor1lem  38054  reheibor  38084  elrfirn  43046  isnacs2  43057  isnacs3  43061  fnwe2lem2  43402  lmhmfgima  43435  brtrclfv2  44077  xphe  44131  imo72b2lem2  44517  imo72b2lem1  44519  imo72b2  44522  limccog  45974  liminfval2  46120  imaf1homlem  49460  imaidfu  49463