Theorem imassrn 6036

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

Syntax hints:   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  {cab 2714   ⊆ wss 3889  ⟨cop 4573  ran crn 5632   “ cima 5634

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  0ima  6043  cnvimass  6047  f1imadifssran  6584  fimass  6688  isofrlem  7295  isofr2  7299  f1opw2  7622  imaexg  7864  f1oweALT  7925  frxp  8076  frxp2  8094  frxp3  8101  smores2  8294  naddunif  8629  naddasslem1  8630  naddasslem2  8631  ecss  8695  fopwdom  9023  sbthlem2  9026  sbthlem3  9027  sbthlem5  9029  sbthlem6  9030  ssenen  9089  ssfiALT  9108  fiint  9237  f1opwfi  9266  marypha1lem  9346  unxpwdom2  9503  tz9.12lem1  9711  djuin  9842  acndom2  9976  dfac12lem2  10067  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  enfin1ai  10306  hsmexlem4  10351  hsmexlem5  10352  fpwwe2lem5  10558  fpwwe2lem8  10561  tskuni  10706  limsupgle  15439  limsupval2  15442  limsupgre  15443  isercolllem2  15628  isercoll  15630  unbenlem  16879  imasless  17504  isacs1i  17623  isacs4lem  18510  mgmhmima  18683  mhmima  18793  cntzmhm  19316  f1omvdconj  19421  gsumzaddlem  19896  dmdprdd  19976  dprdfeq0  19999  dprdres  20005  dprdss  20006  dprdz  20007  subgdmdprd  20011  dprd2dlem1  20018  dprd2da  20019  dmdprdsplit2lem  20022  lmhmlsp  21044  frlmsslsp  21776  lindff1  21800  lindfrn  21801  f1lindf  21802  lindfmm  21807  lsslindf  21810  cnclsi  23237  cnprest2  23255  paste  23259  cmpfi  23373  connima  23390  1stcfb  23410  1stckgenlem  23518  kgencn3  23523  xkoco1cn  23622  xkoco2cn  23623  xkococnlem  23624  qtopval2  23661  basqtop  23676  imastopn  23685  kqopn  23699  kqcld  23700  hmeontr  23734  hmeores  23736  hmphdis  23761  cmphaushmeo  23765  qtopf1  23781  uzfbas  23863  elfm  23912  elfm3  23915  rnelfm  23918  cnextcn  24032  tgpconncomp  24078  qustgpopn  24085  tsmsf1o  24110  ustimasn  24193  utopbas  24200  restutop  24202  tgqioo  24765  cnheiborlem  24921  bndth  24925  fmcfil  25239  ovoliunlem1  25469  volsup  25523  uniioombllem4  25553  uniioombllem5  25554  opnmblALT  25570  volsup2  25572  mbfimaopnlem  25622  mbflimsup  25633  itg2gt0  25727  c1liplem1  25963  dvcnvrelem2  25985  mdegleb  26029  mdeglt  26030  mdegldg  26031  mdegxrcl  26032  mdegcl  26034  ig1peu  26140  efifo  26511  dvlog  26615  efopnlem2  26621  efopn  26622  bdayimaon  27657  noetasuplem4  27700  noetainflem4  27704  nobdaymin  27745  nocvxminlem  27746  noeta2  27753  etaslts2  27786  cutbdaybnd2lim  27789  oldf  27829  lrrecfr  27935  negsunif  28047  negbdaylem  28048  bdayons  28268  zssno  28373  f1otrg  28939  axcontlem10  29042  htthlem  30988  shsss  31384  imaelshi  32129  pjimai  32247  gsummpt2co  33109  gsumpart  33124  elrgspnsubrunlem2  33309  lsmsnorb  33451  dimkerim  33771  sitgclbn  34487  sitgaddlemb  34492  eulerpartlemgvv  34520  eulerpartlemgf  34523  coinfliprv  34627  ballotlemsima  34660  ballotlemro  34667  onvf1odlem4  35288  erdsze2lem2  35386  mrsubrn  35695  msubrn  35711  tailf  36557  dissneqlem  37656  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem11  37952  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem19  37960  poimirlem30  37971  itg2addnclem2  37993  itg2gt0cn  37996  ftc1anclem7  38020  ftc1anc  38022  ismtyima  38124  ismtyres  38129  heibor1lem  38130  reheibor  38160  elrfirn  43127  isnacs2  43138  isnacs3  43142  fnwe2lem2  43479  lmhmfgima  43512  brtrclfv2  44154  xphe  44208  imo72b2lem2  44594  imo72b2lem1  44596  imo72b2  44599  limccog  46050  liminfval2  46196  imaf1homlem  49582  imaidfu  49585