Theorem imassrn 6057

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 1888	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4019	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6049	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5863	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3987	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 399  ∃wex 1798   ∈ wcel 2141  {cab 2739   ⊆ wss 3904  ⟨cop 4587  ran crn 5646   “ cima 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5651  df-cnv 5653  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658

This theorem is referenced by:  0ima  6064  cnvimass  6068  f1imadifssran  6603  fimass  6708  isofrlem  7320  isofr2  7324  f1opw2  7647  imaexg  7890  f1oweALT  7949  frxp  8101  frxp2  8119  frxp3  8126  smores2  8320  naddunif  8659  naddasslem1  8660  naddasslem2  8661  ecss  8725  fopwdom  9053  sbthlem2  9056  sbthlem3  9057  sbthlem5  9059  sbthlem6  9060  ssenen  9119  ssfiALT  9138  fiint  9267  f1opwfi  9296  marypha1lem  9376  unxpwdom2  9533  tz9.12lem1  9742  djuin  9873  acndom2  10007  dfac12lem2  10098  isf34lem5  10332  isf34lem7  10333  isf34lem6  10334  enfin1ai  10338  hsmexlem4  10383  hsmexlem5  10384  fpwwe2lem5  10590  fpwwe2lem8  10593  tskuni  10738  limsupgle  15487  limsupval2  15490  limsupgre  15491  isercolllem2  15676  isercoll  15678  unbenlem  16927  imasless  17553  isacs1i  17672  isacs4lem  18559  mgmhmima  18732  mhmima  18842  cntzmhm  19364  f1omvdconj  19469  gsumzaddlem  19944  dmdprdd  20024  dprdfeq0  20047  dprdres  20053  dprdss  20054  dprdz  20055  subgdmdprd  20059  dprd2dlem1  20066  dprd2da  20067  dmdprdsplit2lem  20070  lmhmlsp  21096  frlmsslsp  21828  lindff1  21852  lindfrn  21853  f1lindf  21854  lindfmm  21859  lsslindf  21862  cnclsi  23312  cnprest2  23330  paste  23334  cmpfi  23448  connima  23465  1stcfb  23485  1stckgenlem  23593  kgencn3  23598  xkoco1cn  23697  xkoco2cn  23698  xkococnlem  23699  qtopval2  23736  basqtop  23751  imastopn  23760  kqopn  23774  kqcld  23775  hmeontr  23809  hmeores  23811  hmphdis  23836  cmphaushmeo  23840  qtopf1  23856  uzfbas  23938  elfm  23987  elfm3  23990  rnelfm  23993  cnextcn  24107  tgpconncomp  24153  qustgpopn  24160  tsmsf1o  24185  ustimasn  24268  utopbas  24275  restutop  24277  tgqioo  24840  cnheiborlem  24996  bndth  25000  fmcfil  25314  ovoliunlem1  25544  volsup  25598  uniioombllem4  25628  uniioombllem5  25629  opnmblALT  25645  volsup2  25647  mbfimaopnlem  25697  mbflimsup  25708  itg2gt0  25802  c1liplem1  26038  dvcnvrelem2  26060  mdegleb  26104  mdeglt  26105  mdegldg  26106  mdegxrcl  26107  mdegcl  26109  ig1peu  26215  efifo  26589  dvlog  26693  efopnlem2  26699  efopn  26700  bdayimaon  27734  noetasuplem4  27777  noetainflem4  27781  nobdaymin  27823  nocvxminlem  27824  noeta2  27831  etaslts2  27864  cutbdaybnd2lim  27867  oldf  27907  lrrecfr  28013  negsunif  28125  negbdaylem  28126  bdayons  28346  zssno  28451  f1otrg  29017  axcontlem10  29120  htthlem  31066  shsss  31462  imaelshi  32207  pjimai  32325  gsummpt2co  33189  gsumpart  33204  elrgspnsubrunlem2  33390  lsmsnorb  33538  dimkerim  33885  sitgclbn  34601  sitgaddlemb  34606  eulerpartlemgvv  34634  eulerpartlemgf  34637  coinfliprv  34741  ballotlemsima  34774  ballotlemro  34781  onvf1odlem4  35413  erdsze2lem2  35518  mrsubrn  35827  msubrn  35843  tailf  36699  dissneqlem  37798  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem11  38094  poimirlem12  38095  poimirlem15  38098  poimirlem16  38099  poimirlem19  38102  poimirlem30  38113  itg2addnclem2  38135  itg2gt0cn  38138  ftc1anclem7  38162  ftc1anc  38164  ismtyima  38266  ismtyres  38271  heibor1lem  38272  reheibor  38302  elrfirn  43240  isnacs2  43251  isnacs3  43255  fnwe2lem2  43592  lmhmfgima  43625  brtrclfv2  44267  xphe  44321  imo72b2lem2  44707  imo72b2lem1  44709  imo72b2  44712  limccog  46160  liminfval2  46306  imaf1homlem  49692  imaidfu  49695