Theorem imassrn 5396

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 1784	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 3637	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 5388	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5234	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3607	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  {cab 2596   ⊆ wss 3540  ⟨cop 4131  ran crn 5039   “ cima 5041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  0ima  5401  cnvimass  5404  fimass  5994  fimacnv  6255  isofrlem  6490  isofr2  6494  f1opw2  6786  imaexg  6995  f1oweALT  7043  frxp  7174  smores2  7338  ecss  7675  f1imaen2g  7903  domunsncan  7945  fopwdom  7953  sbthlem2  7956  sbthlem3  7957  sbthlem5  7959  sbthlem6  7960  ssenen  8019  ssfi  8065  fiint  8122  f1opwfi  8153  marypha1lem  8222  unxpwdom2  8376  tz9.12lem1  8533  acndom2  8760  dfac12lem2  8849  isf34lem5  9083  isf34lem7  9084  isf34lem6  9085  enfin1ai  9089  hsmexlem4  9134  hsmexlem5  9135  fpwwe2lem6  9336  fpwwe2lem9  9339  tskuni  9484  limsupgle  14056  limsupval2  14059  limsupgre  14060  isercolllem2  14244  isercoll  14246  unbenlem  15450  imasless  16023  isacs1i  16141  isacs4lem  16991  mhmima  17186  cntzmhm  17594  f1omvdconj  17689  psgnunilem1  17736  gsumzaddlem  18144  dmdprdd  18221  dprdfeq0  18244  dprdres  18250  dprdss  18251  dprdz  18252  subgdmdprd  18256  dprd2dlem1  18263  dprd2da  18264  dmdprdsplit2lem  18267  lmhmlsp  18870  frlmsslsp  19954  lindff1  19978  lindfrn  19979  f1lindf  19980  lindfmm  19985  lsslindf  19988  cnclsi  20886  cnprest2  20904  paste  20908  cmpfi  21021  conima  21038  1stcfb  21058  1stckgenlem  21166  kgencn3  21171  xkoco1cn  21270  xkoco2cn  21271  xkococnlem  21272  qtopval2  21309  basqtop  21324  imastopn  21333  kqopn  21347  kqcld  21348  hmeontr  21382  hmeores  21384  hmphdis  21409  cmphaushmeo  21413  qtopf1  21429  fbasrn  21498  uzfbas  21512  elfm  21561  elfm3  21564  imaelfm  21565  rnelfm  21567  cnextcn  21681  tgpconcomp  21726  qustgpopn  21733  tsmsf1o  21758  ustimasn  21842  utopbas  21849  restutop  21851  qtopbaslem  22372  tgqioo  22411  cnheiborlem  22561  bndth  22565  fmcfil  22878  ovoliunlem1  23077  volsup  23131  uniioombllem4  23160  uniioombllem5  23161  opnmblALT  23177  volsup2  23179  mbfimaopnlem  23228  mbflimsup  23239  itg2gt0  23333  c1liplem1  23563  dvcnvrelem2  23585  mdegleb  23628  mdeglt  23629  mdegldg  23630  mdegxrcl  23631  mdegcl  23633  ig1peu  23735  efifo  24097  dvlog  24197  efopnlem2  24203  efopn  24204  f1otrg  25551  axcontlem10  25653  eupares  26502  eupath2lem3  26506  htthlem  27158  shsss  27556  imaelshi  28301  pjimai  28419  fimarab  28825  gsummpt2co  29111  sitgclbn  29732  sitgaddlemb  29737  eulerpartlemgvv  29765  eulerpartlemgf  29768  coinfliprv  29871  ballotlemsima  29904  ballotlemro  29911  erdsze2lem2  30440  mrsubrn  30664  msubrn  30680  nocvxminlem  31089  nocvxmin  31090  nobndlem1  31091  nobndlem2  31092  tailf  31540  dissneqlem  32363  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem11  32590  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem19  32598  poimirlem30  32609  itg2addnclem2  32632  itg2gt0cn  32635  ftc1anclem7  32661  ftc1anc  32663  ismtyima  32772  ismtyres  32777  heibor1lem  32778  reheibor  32808  elrfirn  36276  isnacs2  36287  isnacs3  36291  fnwe2lem2  36639  lmhmfgima  36672  brtrclfv2  37038  xphe  37095  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  limccog  38687  mgmhmima  41592