Theorem imassrn 6010

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

Syntax hints:   ∧ wa 396  ∃wex 1780   ∈ wcel 2105  {cab 2713   ⊆ wss 3898  ⟨cop 4579  ran crn 5621   “ cima 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-br 5093  df-opab 5155  df-xp 5626  df-cnv 5628  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633

This theorem is referenced by:  0ima  6016  cnvimass  6019  fimass  6672  fimacnvOLD  7004  isofrlem  7267  isofr2  7271  f1opw2  7586  imaexg  7830  f1oweALT  7883  frxp  8034  smores2  8255  ecss  8615  fopwdom  8945  sbthlem2  8949  sbthlem3  8950  sbthlem5  8952  sbthlem6  8953  ssenen  9016  ssfiALT  9039  fiint  9189  f1opwfi  9221  marypha1lem  9290  unxpwdom2  9445  tz9.12lem1  9644  djuin  9775  acndom2  9911  dfac12lem2  10001  isf34lem5  10235  isf34lem7  10236  isf34lem6  10237  enfin1ai  10241  hsmexlem4  10286  hsmexlem5  10287  fpwwe2lem5  10492  fpwwe2lem8  10495  tskuni  10640  limsupgle  15285  limsupval2  15288  limsupgre  15289  isercolllem2  15476  isercoll  15478  unbenlem  16706  imasless  17348  isacs1i  17463  isacs4lem  18359  mhmima  18560  cntzmhm  19041  f1omvdconj  19150  gsumzaddlem  19617  dmdprdd  19697  dprdfeq0  19720  dprdres  19726  dprdss  19727  dprdz  19728  subgdmdprd  19732  dprd2dlem1  19739  dprd2da  19740  dmdprdsplit2lem  19743  lmhmlsp  20417  frlmsslsp  21109  lindff1  21133  lindfrn  21134  f1lindf  21135  lindfmm  21140  lsslindf  21143  cnclsi  22529  cnprest2  22547  paste  22551  cmpfi  22665  connima  22682  1stcfb  22702  1stckgenlem  22810  kgencn3  22815  xkoco1cn  22914  xkoco2cn  22915  xkococnlem  22916  qtopval2  22953  basqtop  22968  imastopn  22977  kqopn  22991  kqcld  22992  hmeontr  23026  hmeores  23028  hmphdis  23053  cmphaushmeo  23057  qtopf1  23073  uzfbas  23155  elfm  23204  elfm3  23207  rnelfm  23210  cnextcn  23324  tgpconncomp  23370  qustgpopn  23377  tsmsf1o  23402  ustimasn  23486  utopbas  23493  restutop  23495  tgqioo  24069  cnheiborlem  24223  bndth  24227  fmcfil  24542  ovoliunlem1  24772  volsup  24826  uniioombllem4  24856  uniioombllem5  24857  opnmblALT  24873  volsup2  24875  mbfimaopnlem  24925  mbflimsup  24936  itg2gt0  25031  c1liplem1  25266  dvcnvrelem2  25288  mdegleb  25335  mdeglt  25336  mdegldg  25337  mdegxrcl  25338  mdegcl  25340  ig1peu  25442  efifo  25809  dvlog  25912  efopnlem2  25918  efopn  25919  bdayimaon  26947  noetasuplem4  26990  noetainflem4  26994  nocvxminlem  27023  nocvxmin  27024  noeta2  27030  etasslt2  27059  scutbdaybnd2lim  27062  f1otrg  27521  axcontlem10  27630  htthlem  29567  shsss  29963  imaelshi  30708  pjimai  30826  gsummpt2co  31595  gsumpart  31602  lsmsnorb  31876  dimkerim  32006  sitgclbn  32610  sitgaddlemb  32615  eulerpartlemgvv  32643  eulerpartlemgf  32646  coinfliprv  32749  ballotlemsima  32782  ballotlemro  32789  erdsze2lem2  33465  mrsubrn  33774  msubrn  33790  frxp2  34073  frxp3  34079  oldf  34137  lrrecfr  34196  tailf  34660  dissneqlem  35624  poimirlem1  35891  poimirlem2  35892  poimirlem3  35893  poimirlem11  35901  poimirlem12  35902  poimirlem15  35905  poimirlem16  35906  poimirlem19  35909  poimirlem30  35920  itg2addnclem2  35942  itg2gt0cn  35945  ftc1anclem7  35969  ftc1anc  35971  ismtyima  36074  ismtyres  36079  heibor1lem  36080  reheibor  36110  imaexALTV  36604  elrfirn  40787  isnacs2  40798  isnacs3  40802  fnwe2lem2  41147  lmhmfgima  41180  brtrclfv2  41664  xphe  41718  imo72b2lem0  42105  imo72b2lem2  42107  imo72b2lem1  42109  imo72b2  42112  limccog  43505  liminfval2  43653  mgmhmima  45715