Theorem imassrn 6071

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

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  {cab 2740   ⊆ wss 3902  ⟨cop 4593  ran crn 5660   “ cima 5662

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 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is used by:  0ima  6078  cnvimass  6082  fimass  6727  isofrlem  7345  isofr2  7349  f1opw2  7673  imaexg  7914  f1oweALT  7973  frxp  8128  frxp2  8146  frxp3  8153  smores2  8347  naddunif  8686  naddasslem1  8687  naddasslem2  8688  ecss  8752  fopwdom  9087  sbthlem2  9090  sbthlem3  9091  sbthlem5  9093  sbthlem6  9094  ssenen  9153  ssfiALT  9172  fiint  9300  f1opwfi  9327  marypha1lem  9407  unxpwdom2  9564  tz9.12lem1  9773  djuin  9927  acndom2  10061  dfac12lem2  10151  isf34lem5  10384  isf34lem7  10385  isf34lem6  10386  enfin1ai  10390  hsmexlem4  10435  hsmexlem5  10436  fpwwe2lem5  10648  fpwwe2lem8  10651  tskuni  10796  limsupgle  15568  limsupval2  15571  limsupgre  15572  isercolllem2  15757  isercoll  15759  unbenlem  17006  imasless  17632  isacs1i  17751  isacs4lem  18638  mgmhmima  18823  mhmima  18940  cntzmhm  19474  f1omvdconj  19579  gsumzaddlem  20054  dmdprdd  20134  dprdfeq0  20157  dprdres  20163  dprdss  20164  dprdz  20165  subgdmdprd  20169  dprd2dlem1  20176  dprd2da  20177  dmdprdsplit2lem  20180  lmhmlsp  21239  frlmsslsp  22015  lindff1  22039  lindfrn  22040  f1lindf  22041  lindfmm  22046  lsslindf  22049  cnclsi  23503  cnprest2  23521  paste  23525  cmpfi  23639  connima  23656  1stcfb  23676  1stckgenlem  23785  kgencn3  23790  xkoco1cn  23889  xkoco2cn  23890  xkococnlem  23891  qtopval2  23928  basqtop  23943  imastopn  23952  kqopn  23966  kqcld  23967  hmeontr  24001  hmeores  24003  hmphdis  24028  cmphaushmeo  24032  qtopf1  24048  uzfbas  24130  elfm  24179  elfm3  24182  rnelfm  24185  cnextcn  24299  tgpconncomp  24345  qustgpopn  24352  tsmsf1o  24377  ustimasn  24460  utopbas  24467  restutop  24469  tgqioo  25032  cnheiborlem  25188  bndth  25192  fmcfil  25506  ovoliunlem1  25736  volsup  25790  uniioombllem4  25820  uniioombllem5  25821  opnmblALT  25837  volsup2  25839  mbfimaopnlem  25889  mbflimsup  25900  itg2gt0  25994  c1liplem1  26230  dvcnvrelem2  26252  mdegleb  26296  mdeglt  26297  mdegldg  26298  mdegxrcl  26299  mdegcl  26301  ig1peu  26407  efifo  26792  dvlog  26896  efopnlem2  26902  efopn  26903  bdayimaon  27937  noetasuplem4  27980  noetainflem4  27984  nobdaymin  28026  nocvxminlem  28027  noeta2  28034  etaslts2  28067  cutbdaybnd2lim  28070  oldf  28110  lrrecfr  28216  negsunif  28328  negbdaylem  28329  bdayons  28549  zssno  28654  cgrabasimass  29265  f1otrg  29335  axcontlem10  29438  htthlem  31406  shsss  31802  imaelshi  32547  pjimai  32665  gsummpt2co  33496  gsumpart  33511  elrgspnsubrunlem2  33696  lsmsnorb  33832  dimkerim  34145  sitgclbn  34862  sitgaddlemb  34867  eulerpartlemgvv  34895  eulerpartlemgf  34898  coinfliprv  35002  ballotlemsima  35035  ballotlemro  35042  onvf1odlem4  35711  erdsze2lem2  35791  mrsubrn  36100  msubrn  36116  tailf  37002  dissneqlem  38102  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem11  38388  poimirlem12  38389  poimirlem15  38392  poimirlem16  38393  poimirlem19  38396  poimirlem30  38407  itg2addnclem2  38429  itg2gt0cn  38432  ftc1anclem7  38456  ftc1anc  38458  ismtyima  38561  ismtyres  38566  heibor1lem  38567  reheibor  38597  elrfirn  43548  isnacs2  43559  isnacs3  43563  fnwe2lem2  43900  lmhmfgima  43933  brtrclfv2  44575  xphe  44629  imo72b2lem2  45015  imo72b2lem1  45017  imo72b2  45020  limccog  46458  liminfval2  46604  imaf1homlem  50041  imaidfu  50044