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

Theorem imassrn 5465
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 1794 . . 3 (∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴)
21ss2abi 3666 . 2 {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
3 dfima3 5457 . 2 (𝐴𝐵) = {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4 dfrn3 5301 . 2 ran 𝐴 = {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
52, 3, 43sstr4i 3636 1 (𝐴𝐵) ⊆ ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 384  wex 1702  wcel 1988  {cab 2606  wss 3567  cop 4174  ran crn 5105  cima 5107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110  df-cnv 5112  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117
This theorem is referenced by:  0ima  5470  cnvimass  5473  fimass  6068  fimacnv  6333  isofrlem  6575  isofr2  6579  f1opw2  6873  imaexg  7088  f1oweALT  7137  frxp  7272  smores2  7436  ecss  7773  f1imaen2g  8002  domunsncan  8045  fopwdom  8053  sbthlem2  8056  sbthlem3  8057  sbthlem5  8059  sbthlem6  8060  ssenen  8119  ssfi  8165  fiint  8222  f1opwfi  8255  marypha1lem  8324  unxpwdom2  8478  tz9.12lem1  8635  acndom2  8862  dfac12lem2  8951  isf34lem5  9185  isf34lem7  9186  isf34lem6  9187  enfin1ai  9191  hsmexlem4  9236  hsmexlem5  9237  fpwwe2lem6  9442  fpwwe2lem9  9445  tskuni  9590  limsupgle  14189  limsupval2  14192  limsupgre  14193  isercolllem2  14377  isercoll  14379  unbenlem  15593  imasless  16181  isacs1i  16299  isacs4lem  17149  mhmima  17344  cntzmhm  17752  f1omvdconj  17847  psgnunilem1  17894  gsumzaddlem  18302  dmdprdd  18379  dprdfeq0  18402  dprdres  18408  dprdss  18409  dprdz  18410  subgdmdprd  18414  dprd2dlem1  18421  dprd2da  18422  dmdprdsplit2lem  18425  lmhmlsp  19030  frlmsslsp  20116  lindff1  20140  lindfrn  20141  f1lindf  20142  lindfmm  20147  lsslindf  20150  cnclsi  21057  cnprest2  21075  paste  21079  cmpfi  21192  connima  21209  1stcfb  21229  1stckgenlem  21337  kgencn3  21342  xkoco1cn  21441  xkoco2cn  21442  xkococnlem  21443  qtopval2  21480  basqtop  21495  imastopn  21504  kqopn  21518  kqcld  21519  hmeontr  21553  hmeores  21555  hmphdis  21580  cmphaushmeo  21584  qtopf1  21600  fbasrn  21669  uzfbas  21683  elfm  21732  elfm3  21735  imaelfm  21736  rnelfm  21738  cnextcn  21852  tgpconncomp  21897  qustgpopn  21904  tsmsf1o  21929  ustimasn  22013  utopbas  22020  restutop  22022  qtopbaslem  22543  tgqioo  22584  cnheiborlem  22734  bndth  22738  fmcfil  23051  ovoliunlem1  23251  volsup  23305  uniioombllem4  23335  uniioombllem5  23336  opnmblALT  23352  volsup2  23354  mbfimaopnlem  23403  mbflimsup  23414  itg2gt0  23508  c1liplem1  23740  dvcnvrelem2  23762  mdegleb  23805  mdeglt  23806  mdegldg  23807  mdegxrcl  23808  mdegcl  23810  ig1peu  23912  efifo  24274  dvlog  24378  efopnlem2  24384  efopn  24385  f1otrg  25732  axcontlem10  25834  htthlem  27744  shsss  28142  imaelshi  28887  pjimai  29005  fimarab  29418  gsummpt2co  29754  sitgclbn  30379  sitgaddlemb  30384  eulerpartlemgvv  30412  eulerpartlemgf  30415  coinfliprv  30518  ballotlemsima  30551  ballotlemro  30558  erdsze2lem2  31160  mrsubrn  31384  msubrn  31400  bdayimaon  31817  nosupbday  31825  noetalem3  31839  noetalem4  31840  nocvxminlem  31867  nocvxmin  31868  tailf  32345  dissneqlem  33158  poimirlem1  33381  poimirlem2  33382  poimirlem3  33383  poimirlem11  33391  poimirlem12  33392  poimirlem15  33395  poimirlem16  33396  poimirlem19  33399  poimirlem30  33410  itg2addnclem2  33433  itg2gt0cn  33436  ftc1anclem7  33462  ftc1anc  33464  ismtyima  33573  ismtyres  33578  heibor1lem  33579  reheibor  33609  elrfirn  37077  isnacs2  37088  isnacs3  37092  fnwe2lem2  37440  lmhmfgima  37473  brtrclfv2  37838  xphe  37895  imo72b2lem0  38285  imo72b2lem2  38287  imo72b2lem1  38291  imo72b2  38295  limccog  39652  liminfval2  39794  mgmhmima  41567
  Copyright terms: Public domain W3C validator