Theorem imassrn 6071

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 1865	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4061	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6063	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5887	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 4023	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 394  ∃wex 1774   ∈ wcel 2099  {cab 2703   ⊆ wss 3947  ⟨cop 4630  ran crn 5674   “ cima 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5295  ax-nul 5302  ax-pr 5424

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3421  df-v 3465  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5145  df-opab 5207  df-xp 5679  df-cnv 5681  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686

This theorem is referenced by:  0ima  6078  cnvimass  6082  fimass  6738  fimacnvOLD  7074  isofrlem  7342  isofr2  7346  f1opw2  7671  imaexg  7916  f1oweALT  7976  frxp  8130  frxp2  8148  frxp3  8155  smores2  8374  naddunif  8713  naddasslem1  8714  naddasslem2  8715  ecss  8772  fopwdom  9108  sbthlem2  9112  sbthlem3  9113  sbthlem5  9115  sbthlem6  9116  ssenen  9179  ssfiALT  9203  fiint  9359  fiintOLD  9360  f1opwfi  9391  marypha1lem  9467  unxpwdom2  9622  tz9.12lem1  9821  djuin  9952  acndom2  10088  dfac12lem2  10178  isf34lem5  10410  isf34lem7  10411  isf34lem6  10412  enfin1ai  10416  hsmexlem4  10461  hsmexlem5  10462  fpwwe2lem5  10667  fpwwe2lem8  10670  tskuni  10815  limsupgle  15472  limsupval2  15475  limsupgre  15476  isercolllem2  15663  isercoll  15665  unbenlem  16903  imasless  17548  isacs1i  17663  isacs4lem  18562  mgmhmima  18701  mhmima  18808  cntzmhm  19329  f1omvdconj  19438  gsumzaddlem  19913  dmdprdd  19993  dprdfeq0  20016  dprdres  20022  dprdss  20023  dprdz  20024  subgdmdprd  20028  dprd2dlem1  20035  dprd2da  20036  dmdprdsplit2lem  20039  lmhmlsp  21021  frlmsslsp  21788  lindff1  21812  lindfrn  21813  f1lindf  21814  lindfmm  21819  lsslindf  21822  cnclsi  23262  cnprest2  23280  paste  23284  cmpfi  23398  connima  23415  1stcfb  23435  1stckgenlem  23543  kgencn3  23548  xkoco1cn  23647  xkoco2cn  23648  xkococnlem  23649  qtopval2  23686  basqtop  23701  imastopn  23710  kqopn  23724  kqcld  23725  hmeontr  23759  hmeores  23761  hmphdis  23786  cmphaushmeo  23790  qtopf1  23806  uzfbas  23888  elfm  23937  elfm3  23940  rnelfm  23943  cnextcn  24057  tgpconncomp  24103  qustgpopn  24110  tsmsf1o  24135  ustimasn  24219  utopbas  24226  restutop  24228  tgqioo  24802  cnheiborlem  24966  bndth  24970  fmcfil  25286  ovoliunlem1  25517  volsup  25571  uniioombllem4  25601  uniioombllem5  25602  opnmblALT  25618  volsup2  25620  mbfimaopnlem  25670  mbflimsup  25681  itg2gt0  25776  c1liplem1  26015  dvcnvrelem2  26037  mdegleb  26086  mdeglt  26087  mdegldg  26088  mdegxrcl  26089  mdegcl  26091  ig1peu  26197  efifo  26569  dvlog  26673  efopnlem2  26679  efopn  26680  bdayimaon  27718  noetasuplem4  27761  noetainflem4  27765  nocvxminlem  27802  nocvxmin  27803  noeta2  27809  etasslt2  27839  scutbdaybnd2lim  27842  oldf  27876  lrrecfr  27952  negsunif  28059  negsbdaylem  28060  zssno  28326  f1otrg  28793  axcontlem10  28902  htthlem  30845  shsss  31241  imaelshi  31986  pjimai  32104  gsummpt2co  32918  gsumpart  32925  lsmsnorb  33270  dimkerim  33526  sitgclbn  34188  sitgaddlemb  34193  eulerpartlemgvv  34221  eulerpartlemgf  34224  coinfliprv  34327  ballotlemsima  34360  ballotlemro  34367  erdsze2lem2  35043  mrsubrn  35352  msubrn  35368  tailf  36098  dissneqlem  37058  poimirlem1  37333  poimirlem2  37334  poimirlem3  37335  poimirlem11  37343  poimirlem12  37344  poimirlem15  37347  poimirlem16  37348  poimirlem19  37351  poimirlem30  37362  itg2addnclem2  37384  itg2gt0cn  37387  ftc1anclem7  37411  ftc1anc  37413  ismtyima  37515  ismtyres  37520  heibor1lem  37521  reheibor  37551  imaexALTV  38039  elrfirn  42387  isnacs2  42398  isnacs3  42402  fnwe2lem2  42747  lmhmfgima  42780  brtrclfv2  43429  xphe  43483  imo72b2lem0  43867  imo72b2lem2  43869  imo72b2lem1  43871  imo72b2  43874  limccog  45275  liminfval2  45423