Theorem imassrn 6197

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 3932	. . 3 ⊢ 𝐵 ⊆ V
2		imass2 6054	. . 3 ⊢ (𝐵 ⊆ V → (𝐴 “ 𝐵) ⊆ (𝐴 “ V))
3	1, 2	ax-mp 5	. 2 ⊢ (𝐴 “ 𝐵) ⊆ (𝐴 “ V)
4		dfrn4 6196	. 2 ⊢ ran 𝐴 = (𝐴 “ V)
5	3, 4	sseqtrri 3957	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

This proof depends on syntax axioms:  Vcvv 3450   ⊆ wss 3895  ran crn 5651   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  cnvimass  6198  0ima  6200  fimass  6730  isofrlem  7348  isofr2  7352  f1opw2  7676  imaexg  7925  f1oweALT  7984  frxp  8140  frxp2  8163  frxp3  8170  smores2  8365  naddunif  8706  naddasslem1  8707  naddasslem2  8708  ecss  8772  fopwdom  9107  sbthlem2  9110  sbthlem3  9111  sbthlem5  9113  sbthlem6  9114  ssenen  9173  ssfiALT  9192  fiint  9321  f1opwfi  9348  marypha1lem  9428  unxpwdom2  9585  tz9.12lem1  9797  djuin  10002  acndom2  10136  dfac12lem2  10226  isf34lem5  10459  isf34lem7  10460  isf34lem6  10461  enfin1ai  10465  hsmexlem4  10510  hsmexlem5  10511  fpwwe2lem5  10723  fpwwe2lem8  10726  tskuni  10871  limsupgle  15649  limsupval2  15652  limsupgre  15653  isercolllem2  15838  isercoll  15840  unbenlem  17091  imasless  17717  isacs1i  17836  isacs4lem  18723  mgmhmima  18909  mhmima  19026  cntzmhm  19560  f1omvdconj  19665  gsumzaddlem  20140  dmdprdd  20220  dprdfeq0  20243  dprdres  20249  dprdss  20250  dprdz  20251  subgdmdprd  20255  dprd2dlem1  20262  dprd2da  20263  dmdprdsplit2lem  20266  lmhmlsp  21329  frlmsslsp  22107  lindff1  22131  lindfrn  22132  f1lindf  22133  lindfmm  22138  lsslindf  22141  cnclsi  23595  cnprest2  23613  paste  23617  cmpfi  23731  connima  23748  1stcfb  23768  1stckgenlem  23877  kgencn3  23882  xkoco1cn  23981  xkoco2cn  23982  xkococnlem  23983  qtopval2  24020  basqtop  24035  imastopn  24044  kqopn  24058  kqcld  24059  hmeontr  24093  hmeores  24095  hmphdis  24120  cmphaushmeo  24124  qtopf1  24140  uzfbas  24222  elfm  24271  elfm3  24274  rnelfm  24277  cnextcn  24391  tgpconncomp  24437  qustgpopn  24444  tsmsf1o  24469  ustimasn  24552  utopbas  24559  restutop  24561  tgqioo  25124  cnheiborlem  25280  bndth  25284  fmcfil  25598  ovoliunlem1  25828  volsup  25882  uniioombllem4  25912  uniioombllem5  25913  opnmblALT  25929  volsup2  25931  mbfimaopnlem  25981  mbflimsup  25992  itg2gt0  26086  c1liplem1  26321  dvcnvrelem2  26343  mdegleb  26387  mdeglt  26388  mdegldg  26389  mdegxrcl  26390  mdegcl  26392  ig1peu  26498  efifo  26880  dvlog  26984  efopnlem2  26990  efopn  26991  bdayimaon  28055  noetasuplem4  28098  noetainflem4  28102  nobdaymin  28144  nocvxminlem  28145  noeta2  28152  etaslts2  28185  cutbdaybnd2lim  28188  oldf  28228  lrrecfr  28334  negsunif  28446  negbdaylem  28447  bdayons  28667  zssno  28772  cgrabasimass  29383  f1otrg  29453  axcontlem10  29556  htthlem  31524  shsss  31920  imaelshi  32665  pjimai  32783  gsummpt2co  33655  gsumpart  33670  elrgspnsubrunlem2  33855  lsmsnorb  33992  dimkerim  34305  sitgclbn  35021  sitgaddlemb  35026  eulerpartlemgvv  35054  eulerpartlemgf  35057  coinfliprv  35161  ballotlemsima  35194  ballotlemro  35201  acwer1prc  35816  j0ltalephlem  35946  onvf1odlem4  35953  erdsze2lem2  36055  mrsubrn  36364  msubrn  36380  tailf  37255  dissneqlem  38356  poimirlem1  38632  poimirlem2  38633  poimirlem3  38634  poimirlem11  38642  poimirlem12  38643  poimirlem15  38646  poimirlem16  38647  poimirlem19  38650  poimirlem30  38661  itg2addnclem2  38683  itg2gt0cn  38686  ftc1anclem7  38710  ftc1anc  38712  ismtyima  38830  ismtyres  38835  heibor1lem  38836  reheibor  38866  elrfirn  43799  isnacs2  43810  isnacs3  43814  lmhmfgima  44179  brtrclfv2  44820  xphe  44874  imo72b2lem2  45260  imo72b2lem1  45262  imo72b2  45265  limccog  46725  liminfval2  46871  imaf1homlem  50316  imaidfu  50319