MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imassrn Structured version   Visualization version   GIF version

Theorem imassrn 5934
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.
StepHypRef Expression
1 exsimpr 1861 . . 3 (∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴)
21ss2abi 4042 . 2 {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
3 dfima3 5926 . 2 (𝐴𝐵) = {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4 dfrn3 5754 . 2 ran 𝐴 = {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
52, 3, 43sstr4i 4009 1 (𝐴𝐵) ⊆ ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 396  wex 1771  wcel 2105  {cab 2799  wss 3935  cop 4565  ran crn 5550  cima 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-xp 5555  df-cnv 5557  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562
This theorem is referenced by:  0ima  5940  cnvimass  5943  fimass  6549  fimacnv  6832  isofrlem  7082  isofr2  7086  f1opw2  7389  imaexg  7608  f1oweALT  7664  frxp  7811  smores2  7982  ecss  8325  fopwdom  8614  sbthlem2  8617  sbthlem3  8618  sbthlem5  8620  sbthlem6  8621  ssenen  8680  ssfi  8727  fiint  8784  f1opwfi  8817  marypha1lem  8886  unxpwdom2  9041  tz9.12lem1  9205  djuin  9336  acndom2  9469  dfac12lem2  9559  isf34lem5  9789  isf34lem7  9790  isf34lem6  9791  enfin1ai  9795  hsmexlem4  9840  hsmexlem5  9841  fpwwe2lem6  10046  fpwwe2lem9  10049  tskuni  10194  limsupgle  14824  limsupval2  14827  limsupgre  14828  isercolllem2  15012  isercoll  15014  unbenlem  16234  imasless  16803  isacs1i  16918  isacs4lem  17768  mhmima  17979  cntzmhm  18409  f1omvdconj  18505  gsumzaddlem  18972  dmdprdd  19052  dprdfeq0  19075  dprdres  19081  dprdss  19082  dprdz  19083  subgdmdprd  19087  dprd2dlem1  19094  dprd2da  19095  dmdprdsplit2lem  19098  lmhmlsp  19752  frlmsslsp  20870  lindff1  20894  lindfrn  20895  f1lindf  20896  lindfmm  20901  lsslindf  20904  cnclsi  21810  cnprest2  21828  paste  21832  cmpfi  21946  connima  21963  1stcfb  21983  1stckgenlem  22091  kgencn3  22096  xkoco1cn  22195  xkoco2cn  22196  xkococnlem  22197  qtopval2  22234  basqtop  22249  imastopn  22258  kqopn  22272  kqcld  22273  hmeontr  22307  hmeores  22309  hmphdis  22334  cmphaushmeo  22338  qtopf1  22354  uzfbas  22436  elfm  22485  elfm3  22488  rnelfm  22491  cnextcn  22605  tgpconncomp  22650  qustgpopn  22657  tsmsf1o  22682  ustimasn  22766  utopbas  22773  restutop  22775  tgqioo  23337  cnheiborlem  23487  bndth  23491  fmcfil  23804  ovoliunlem1  24032  volsup  24086  uniioombllem4  24116  uniioombllem5  24117  opnmblALT  24133  volsup2  24135  mbfimaopnlem  24185  mbflimsup  24196  itg2gt0  24290  c1liplem1  24522  dvcnvrelem2  24544  mdegleb  24587  mdeglt  24588  mdegldg  24589  mdegxrcl  24590  mdegcl  24592  ig1peu  24694  efifo  25058  dvlog  25161  efopnlem2  25167  efopn  25168  f1otrg  26585  axcontlem10  26687  htthlem  28622  shsss  29018  imaelshi  29763  pjimai  29881  gsummpt2co  30614  dimkerim  30923  sitgclbn  31501  sitgaddlemb  31506  eulerpartlemgvv  31534  eulerpartlemgf  31537  coinfliprv  31640  ballotlemsima  31673  ballotlemro  31680  erdsze2lem2  32349  mrsubrn  32658  msubrn  32674  bdayimaon  33095  nosupbday  33103  noetalem3  33117  noetalem4  33118  nocvxminlem  33145  nocvxmin  33146  tailf  33621  dissneqlem  34504  poimirlem1  34775  poimirlem2  34776  poimirlem3  34777  poimirlem11  34785  poimirlem12  34786  poimirlem15  34789  poimirlem16  34790  poimirlem19  34793  poimirlem30  34804  itg2addnclem2  34826  itg2gt0cn  34829  ftc1anclem7  34855  ftc1anc  34857  ismtyima  34964  ismtyres  34969  heibor1lem  34970  reheibor  35000  imaexALTV  35470  elrfirn  39172  isnacs2  39183  isnacs3  39187  fnwe2lem2  39531  lmhmfgima  39564  brtrclfv2  39952  xphe  40007  imo72b2lem0  40396  imo72b2lem2  40398  imo72b2lem1  40402  imo72b2  40406  limccog  41781  liminfval2  41929  mgmhmima  43916
  Copyright terms: Public domain W3C validator