Theorem imassrn 5969

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 1873	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 3996	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 5961	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5787	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3960	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  {cab 2715   ⊆ wss 3883  ⟨cop 4564  ran crn 5581   “ cima 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593

This theorem is referenced by:  0ima  5975  cnvimass  5978  fimass  6605  fimacnvOLD  6930  isofrlem  7191  isofr2  7195  f1opw2  7502  imaexg  7736  f1oweALT  7788  frxp  7938  smores2  8156  ecss  8502  fopwdom  8820  sbthlem2  8824  sbthlem3  8825  sbthlem5  8827  sbthlem6  8828  ssenen  8887  ssfiALT  8919  fiint  9021  f1opwfi  9053  marypha1lem  9122  unxpwdom2  9277  tz9.12lem1  9476  djuin  9607  acndom2  9741  dfac12lem2  9831  isf34lem5  10065  isf34lem7  10066  isf34lem6  10067  enfin1ai  10071  hsmexlem4  10116  hsmexlem5  10117  fpwwe2lem5  10322  fpwwe2lem8  10325  tskuni  10470  limsupgle  15114  limsupval2  15117  limsupgre  15118  isercolllem2  15305  isercoll  15307  unbenlem  16537  imasless  17168  isacs1i  17283  isacs4lem  18177  mhmima  18378  cntzmhm  18860  f1omvdconj  18969  gsumzaddlem  19437  dmdprdd  19517  dprdfeq0  19540  dprdres  19546  dprdss  19547  dprdz  19548  subgdmdprd  19552  dprd2dlem1  19559  dprd2da  19560  dmdprdsplit2lem  19563  lmhmlsp  20226  frlmsslsp  20913  lindff1  20937  lindfrn  20938  f1lindf  20939  lindfmm  20944  lsslindf  20947  cnclsi  22331  cnprest2  22349  paste  22353  cmpfi  22467  connima  22484  1stcfb  22504  1stckgenlem  22612  kgencn3  22617  xkoco1cn  22716  xkoco2cn  22717  xkococnlem  22718  qtopval2  22755  basqtop  22770  imastopn  22779  kqopn  22793  kqcld  22794  hmeontr  22828  hmeores  22830  hmphdis  22855  cmphaushmeo  22859  qtopf1  22875  uzfbas  22957  elfm  23006  elfm3  23009  rnelfm  23012  cnextcn  23126  tgpconncomp  23172  qustgpopn  23179  tsmsf1o  23204  ustimasn  23288  utopbas  23295  restutop  23297  tgqioo  23869  cnheiborlem  24023  bndth  24027  fmcfil  24341  ovoliunlem1  24571  volsup  24625  uniioombllem4  24655  uniioombllem5  24656  opnmblALT  24672  volsup2  24674  mbfimaopnlem  24724  mbflimsup  24735  itg2gt0  24830  c1liplem1  25065  dvcnvrelem2  25087  mdegleb  25134  mdeglt  25135  mdegldg  25136  mdegxrcl  25137  mdegcl  25139  ig1peu  25241  efifo  25608  dvlog  25711  efopnlem2  25717  efopn  25718  f1otrg  27136  axcontlem10  27244  htthlem  29180  shsss  29576  imaelshi  30321  pjimai  30439  gsummpt2co  31210  gsumpart  31217  lsmsnorb  31481  dimkerim  31610  sitgclbn  32210  sitgaddlemb  32215  eulerpartlemgvv  32243  eulerpartlemgf  32246  coinfliprv  32349  ballotlemsima  32382  ballotlemro  32389  erdsze2lem2  33066  mrsubrn  33375  msubrn  33391  frxp2  33718  frxp3  33724  bdayimaon  33823  noetasuplem4  33866  noetainflem4  33870  nocvxminlem  33899  nocvxmin  33900  noeta2  33906  etasslt2  33935  scutbdaybnd2lim  33938  oldf  33968  lrrecfr  34027  tailf  34491  dissneqlem  35438  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem11  35715  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem19  35723  poimirlem30  35734  itg2addnclem2  35756  itg2gt0cn  35759  ftc1anclem7  35783  ftc1anc  35785  ismtyima  35888  ismtyres  35893  heibor1lem  35894  reheibor  35924  imaexALTV  36392  elrfirn  40433  isnacs2  40444  isnacs3  40448  fnwe2lem2  40792  lmhmfgima  40825  brtrclfv2  41224  xphe  41278  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2lem1  41669  imo72b2  41672  limccog  43051  liminfval2  43199  mgmhmima  45244