Theorem imassrn 6064

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 1892	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4022	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6056	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5870	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3990	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 400  ∃wex 1802   ∈ wcel 2145  {cab 2743   ⊆ wss 3907  ⟨cop 4591  ran crn 5653   “ cima 5655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-xp 5658  df-cnv 5660  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665

This theorem is referenced by:  0ima  6071  cnvimass  6075  f1imadifssran  6611  fimass  6716  isofrlem  7328  isofr2  7332  f1opw2  7655  imaexg  7898  f1oweALT  7957  frxp  8110  frxp2  8128  frxp3  8135  smores2  8329  naddunif  8668  naddasslem1  8669  naddasslem2  8670  ecss  8734  fopwdom  9061  sbthlem2  9064  sbthlem3  9065  sbthlem5  9067  sbthlem6  9068  ssenen  9127  ssfiALT  9146  fiint  9274  f1opwfi  9301  marypha1lem  9381  unxpwdom2  9538  tz9.12lem1  9747  djuin  9892  acndom2  10026  dfac12lem2  10116  isf34lem5  10350  isf34lem7  10351  isf34lem6  10352  enfin1ai  10356  hsmexlem4  10401  hsmexlem5  10402  fpwwe2lem5  10608  fpwwe2lem8  10611  tskuni  10756  limsupgle  15518  limsupval2  15521  limsupgre  15522  isercolllem2  15707  isercoll  15709  unbenlem  16958  imasless  17584  isacs1i  17703  isacs4lem  18590  mgmhmima  18763  mhmima  18874  cntzmhm  19402  f1omvdconj  19507  gsumzaddlem  19982  dmdprdd  20062  dprdfeq0  20085  dprdres  20091  dprdss  20092  dprdz  20093  subgdmdprd  20097  dprd2dlem1  20104  dprd2da  20105  dmdprdsplit2lem  20108  lmhmlsp  21139  frlmsslsp  21906  lindff1  21930  lindfrn  21931  f1lindf  21932  lindfmm  21937  lsslindf  21940  cnclsi  23390  cnprest2  23408  paste  23412  cmpfi  23526  connima  23543  1stcfb  23563  1stckgenlem  23671  kgencn3  23676  xkoco1cn  23775  xkoco2cn  23776  xkococnlem  23777  qtopval2  23814  basqtop  23829  imastopn  23838  kqopn  23852  kqcld  23853  hmeontr  23887  hmeores  23889  hmphdis  23914  cmphaushmeo  23918  qtopf1  23934  uzfbas  24016  elfm  24065  elfm3  24068  rnelfm  24071  cnextcn  24185  tgpconncomp  24231  qustgpopn  24238  tsmsf1o  24263  ustimasn  24346  utopbas  24353  restutop  24355  tgqioo  24918  cnheiborlem  25074  bndth  25078  fmcfil  25392  ovoliunlem1  25622  volsup  25676  uniioombllem4  25706  uniioombllem5  25707  opnmblALT  25723  volsup2  25725  mbfimaopnlem  25775  mbflimsup  25786  itg2gt0  25880  c1liplem1  26116  dvcnvrelem2  26138  mdegleb  26182  mdeglt  26183  mdegldg  26184  mdegxrcl  26185  mdegcl  26187  ig1peu  26293  efifo  26670  dvlog  26774  efopnlem2  26780  efopn  26781  bdayimaon  27815  noetasuplem4  27858  noetainflem4  27862  nobdaymin  27904  nocvxminlem  27905  noeta2  27912  etaslts2  27945  cutbdaybnd2lim  27948  oldf  27988  lrrecfr  28094  negsunif  28206  negbdaylem  28207  bdayons  28427  zssno  28532  f1otrg  29129  axcontlem10  29232  htthlem  31178  shsss  31574  imaelshi  32319  pjimai  32437  gsummpt2co  33281  gsumpart  33296  elrgspnsubrunlem2  33481  lsmsnorb  33620  dimkerim  33934  sitgclbn  34650  sitgaddlemb  34655  eulerpartlemgvv  34683  eulerpartlemgf  34686  coinfliprv  34790  ballotlemsima  34823  ballotlemro  34830  onvf1odlem4  35461  erdsze2lem2  35567  mrsubrn  35876  msubrn  35892  tailf  36748  dissneqlem  37846  poimirlem1  38132  poimirlem2  38133  poimirlem3  38134  poimirlem11  38142  poimirlem12  38143  poimirlem15  38146  poimirlem16  38147  poimirlem19  38150  poimirlem30  38161  itg2addnclem2  38183  itg2gt0cn  38186  ftc1anclem7  38210  ftc1anc  38212  ismtyima  38314  ismtyres  38319  heibor1lem  38320  reheibor  38350  elrfirn  43288  isnacs2  43299  isnacs3  43303  fnwe2lem2  43640  lmhmfgima  43673  brtrclfv2  44315  xphe  44369  imo72b2lem2  44755  imo72b2lem1  44757  imo72b2  44760  limccog  46194  liminfval2  46340  imaf1homlem  49736  imaidfu  49739