Theorem imassrn 6030

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

Syntax hints:   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  {cab 2715   ⊆ wss 3890  ⟨cop 4574  ran crn 5625   “ cima 5627

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 5231  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  0ima  6037  cnvimass  6041  f1imadifssran  6578  fimass  6682  isofrlem  7288  isofr2  7292  f1opw2  7615  imaexg  7857  f1oweALT  7918  frxp  8069  frxp2  8087  frxp3  8094  smores2  8287  naddunif  8622  naddasslem1  8623  naddasslem2  8624  ecss  8688  fopwdom  9016  sbthlem2  9019  sbthlem3  9020  sbthlem5  9022  sbthlem6  9023  ssenen  9082  ssfiALT  9101  fiint  9230  f1opwfi  9259  marypha1lem  9339  unxpwdom2  9496  tz9.12lem1  9702  djuin  9833  acndom2  9967  dfac12lem2  10058  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  enfin1ai  10297  hsmexlem4  10342  hsmexlem5  10343  fpwwe2lem5  10549  fpwwe2lem8  10552  tskuni  10697  limsupgle  15430  limsupval2  15433  limsupgre  15434  isercolllem2  15619  isercoll  15621  unbenlem  16870  imasless  17495  isacs1i  17614  isacs4lem  18501  mgmhmima  18674  mhmima  18784  cntzmhm  19307  f1omvdconj  19412  gsumzaddlem  19887  dmdprdd  19967  dprdfeq0  19990  dprdres  19996  dprdss  19997  dprdz  19998  subgdmdprd  20002  dprd2dlem1  20009  dprd2da  20010  dmdprdsplit2lem  20013  lmhmlsp  21036  frlmsslsp  21786  lindff1  21810  lindfrn  21811  f1lindf  21812  lindfmm  21817  lsslindf  21820  cnclsi  23247  cnprest2  23265  paste  23269  cmpfi  23383  connima  23400  1stcfb  23420  1stckgenlem  23528  kgencn3  23533  xkoco1cn  23632  xkoco2cn  23633  xkococnlem  23634  qtopval2  23671  basqtop  23686  imastopn  23695  kqopn  23709  kqcld  23710  hmeontr  23744  hmeores  23746  hmphdis  23771  cmphaushmeo  23775  qtopf1  23791  uzfbas  23873  elfm  23922  elfm3  23925  rnelfm  23928  cnextcn  24042  tgpconncomp  24088  qustgpopn  24095  tsmsf1o  24120  ustimasn  24203  utopbas  24210  restutop  24212  tgqioo  24775  cnheiborlem  24931  bndth  24935  fmcfil  25249  ovoliunlem1  25479  volsup  25533  uniioombllem4  25563  uniioombllem5  25564  opnmblALT  25580  volsup2  25582  mbfimaopnlem  25632  mbflimsup  25643  itg2gt0  25737  c1liplem1  25973  dvcnvrelem2  25995  mdegleb  26039  mdeglt  26040  mdegldg  26041  mdegxrcl  26042  mdegcl  26044  ig1peu  26150  efifo  26524  dvlog  26628  efopnlem2  26634  efopn  26635  bdayimaon  27671  noetasuplem4  27714  noetainflem4  27718  nobdaymin  27759  nocvxminlem  27760  noeta2  27767  etaslts2  27800  cutbdaybnd2lim  27803  oldf  27843  lrrecfr  27949  negsunif  28061  negbdaylem  28062  bdayons  28282  zssno  28387  f1otrg  28953  axcontlem10  29056  htthlem  31003  shsss  31399  imaelshi  32144  pjimai  32262  gsummpt2co  33124  gsumpart  33139  elrgspnsubrunlem2  33324  lsmsnorb  33466  dimkerim  33787  sitgclbn  34503  sitgaddlemb  34508  eulerpartlemgvv  34536  eulerpartlemgf  34539  coinfliprv  34643  ballotlemsima  34676  ballotlemro  34683  onvf1odlem4  35304  erdsze2lem2  35402  mrsubrn  35711  msubrn  35727  tailf  36573  dissneqlem  37670  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem11  37966  poimirlem12  37967  poimirlem15  37970  poimirlem16  37971  poimirlem19  37974  poimirlem30  37985  itg2addnclem2  38007  itg2gt0cn  38010  ftc1anclem7  38034  ftc1anc  38036  ismtyima  38138  ismtyres  38143  heibor1lem  38144  reheibor  38174  elrfirn  43141  isnacs2  43152  isnacs3  43156  fnwe2lem2  43497  lmhmfgima  43530  brtrclfv2  44172  xphe  44226  imo72b2lem2  44612  imo72b2lem1  44614  imo72b2  44617  limccog  46068  liminfval2  46214  imaf1homlem  49594  imaidfu  49597