Theorem imassrn 6210

Description: Any image by a class is included in the range of the class. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.) (Proof shortened by BJ, 27-Sep-2026.)

Assertion

Ref	Expression
imassrn	⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Proof of Theorem imassrn

Step	Hyp	Ref	Expression
1		ssv 3937	. . 3 ⊢ 𝐵 ⊆ V
2		imass2 6067	. . 3 ⊢ (𝐵 ⊆ V → (𝐴 “ 𝐵) ⊆ (𝐴 “ V))
3	1, 2	ax-mp 5	. 2 ⊢ (𝐴 “ 𝐵) ⊆ (𝐴 “ V)
4		dfrn4 6209	. 2 ⊢ ran 𝐴 = (𝐴 “ V)
5	3, 4	sseqtrri 3962	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

This proof depends on syntax axioms:  Vcvv 3454   ⊆ wss 3900  ran crn 5656   “ cima 5658

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  cnvimass  6211  0ima  6213  fimass  6752  isofrlem  7371  isofr2  7375  f1opw2  7700  imaexg  7949  f1oweALT  8008  frxp  8165  frxp2  8188  frxp3  8195  smores2  8390  naddunif  8731  naddasslem1  8732  naddasslem2  8733  ecss  8797  fopwdom  9132  sbthlem2  9135  sbthlem3  9136  sbthlem5  9138  sbthlem6  9139  ssenen  9198  ssfiALT  9217  fiint  9346  f1opwfi  9373  marypha1lem  9452  unxpwdom2  9609  tz9.12lem1  9821  djuin  10026  acndom2  10160  dfac12lem2  10250  isf34lem5  10483  isf34lem7  10484  isf34lem6  10485  enfin1ai  10489  hsmexlem4  10534  hsmexlem5  10535  fpwwe2lem5  10747  fpwwe2lem8  10750  tskuni  10895  limsupgle  15673  limsupval2  15676  limsupgre  15677  isercolllem2  15862  isercoll  15864  unbenlem  17115  imasless  17741  isacs1i  17860  isacs4lem  18747  mgmhmima  18933  mhmima  19050  cntzmhm  19585  f1omvdconj  19690  gsumzaddlem  20165  dmdprdd  20245  dprdfeq0  20268  dprdres  20274  dprdss  20275  dprdz  20276  subgdmdprd  20280  dprd2dlem1  20287  dprd2da  20288  dmdprdsplit2lem  20291  lmhmlsp  21354  frlmsslsp  22132  lindff1  22156  lindfrn  22157  f1lindf  22158  lindfmm  22163  lsslindf  22166  cnclsi  23620  cnprest2  23638  paste  23642  cmpfi  23756  connima  23773  1stcfb  23793  1stckgenlem  23902  kgencn3  23907  xkoco1cn  24006  xkoco2cn  24007  xkococnlem  24008  qtopval2  24045  basqtop  24060  imastopn  24069  kqopn  24083  kqcld  24084  hmeontr  24118  hmeores  24120  hmphdis  24145  cmphaushmeo  24149  qtopf1  24165  uzfbas  24247  elfm  24296  elfm3  24299  rnelfm  24302  cnextcn  24416  tgpconncomp  24462  qustgpopn  24469  tsmsf1o  24494  ustimasn  24577  utopbas  24584  restutop  24586  tgqioo  25149  cnheiborlem  25305  bndth  25309  fmcfil  25623  ovoliunlem1  25853  volsup  25907  uniioombllem4  25937  uniioombllem5  25938  opnmblALT  25954  volsup2  25956  mbfimaopnlem  26006  mbflimsup  26017  itg2gt0  26111  c1liplem1  26346  dvcnvrelem2  26368  mdegleb  26412  mdeglt  26413  mdegldg  26414  mdegxrcl  26415  mdegcl  26417  ig1peu  26523  efifo  26905  dvlog  27009  efopnlem2  27015  efopn  27016  bdayimaon  28080  noetasuplem4  28123  noetainflem4  28127  nobdaymin  28169  nocvxminlem  28170  noeta2  28177  etaslts2  28210  cutbdaybnd2lim  28213  oldf  28253  lrrecfr  28359  negsunif  28471  negbdaylem  28472  bdayons  28692  zssno  28797  cgrabasimass  29408  f1otrg  29478  axcontlem10  29581  htthlem  31549  shsss  31945  imaelshi  32690  pjimai  32808  gsummpt2co  33679  gsumpart  33694  elrgspnsubrunlem2  33879  lsmsnorb  34016  dimkerim  34329  sitgclbn  35045  sitgaddlemb  35050  eulerpartlemgvv  35078  eulerpartlemgf  35081  coinfliprv  35185  ballotlemsima  35218  ballotlemro  35225  acwer1prc  35852  j0ltalephlem  36007  onvf1odlem4  36034  erdsze2lem2  36136  mrsubrn  36445  msubrn  36461  tailf  37341  dissneqlem  38455  poimirlem1  38731  poimirlem2  38732  poimirlem3  38733  poimirlem11  38741  poimirlem12  38742  poimirlem15  38745  poimirlem16  38746  poimirlem19  38749  poimirlem30  38760  itg2addnclem2  38782  itg2gt0cn  38785  ftc1anclem7  38809  ftc1anc  38811  ismtyima  38929  ismtyres  38934  heibor1lem  38935  reheibor  38965  elrfirn  43899  isnacs2  43910  isnacs3  43914  lmhmfgima  44279  brtrclfv2  44919  xphe  44973  imo72b2lem2  45359  imo72b2lem1  45361  imo72b2  45364  limccog  46837  liminfval2  46983  imaf1homlem  50428  imaidfu  50431