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

Theorem imassrn 5380
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 1783 . . 3 (∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴)
21ss2abi 3633 . 2 {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
3 dfima3 5372 . 2 (𝐴𝐵) = {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4 dfrn3 5219 . 2 ran 𝐴 = {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
52, 3, 43sstr4i 3603 1 (𝐴𝐵) ⊆ ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 382  wex 1694  wcel 1976  {cab 2592  wss 3536  cop 4127  ran crn 5026  cima 5028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-xp 5031  df-cnv 5033  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038
This theorem is referenced by:  0ima  5385  cnvimass  5388  fimass  5976  fimacnv  6237  isofrlem  6465  isofr2  6469  f1opw2  6760  imaexg  6969  f1oweALT  7017  frxp  7148  smores2  7312  ecss  7649  f1imaen2g  7877  domunsncan  7919  fopwdom  7927  sbthlem2  7930  sbthlem3  7931  sbthlem5  7933  sbthlem6  7934  ssenen  7993  ssfi  8039  fiint  8096  f1opwfi  8127  marypha1lem  8196  unxpwdom2  8350  tz9.12lem1  8507  acndom2  8734  dfac12lem2  8823  isf34lem5  9057  isf34lem7  9058  isf34lem6  9059  enfin1ai  9063  hsmexlem4  9108  hsmexlem5  9109  fpwwe2lem6  9310  fpwwe2lem9  9313  tskuni  9458  limsupgle  13999  limsupval2  14002  limsupgre  14003  isercolllem2  14187  isercoll  14189  unbenlem  15393  imasless  15966  isacs1i  16084  isacs4lem  16934  mhmima  17129  cntzmhm  17537  f1omvdconj  17632  psgnunilem1  17679  gsumzaddlem  18087  dmdprdd  18164  dprdfeq0  18187  dprdres  18193  dprdss  18194  dprdz  18195  subgdmdprd  18199  dprd2dlem1  18206  dprd2da  18207  dmdprdsplit2lem  18210  lmhmlsp  18813  frlmsslsp  19893  lindff1  19917  lindfrn  19918  f1lindf  19919  lindfmm  19924  lsslindf  19927  cnclsi  20825  cnprest2  20843  paste  20847  cmpfi  20960  conima  20977  1stcfb  20997  1stckgenlem  21105  kgencn3  21110  xkoco1cn  21209  xkoco2cn  21210  xkococnlem  21211  qtopval2  21248  basqtop  21263  imastopn  21272  kqopn  21286  kqcld  21287  hmeontr  21321  hmeores  21323  hmphdis  21348  cmphaushmeo  21352  qtopf1  21368  fbasrn  21437  uzfbas  21451  elfm  21500  elfm3  21503  imaelfm  21504  rnelfm  21506  cnextcn  21620  tgpconcomp  21665  qustgpopn  21672  tsmsf1o  21697  ustimasn  21781  utopbas  21788  restutop  21790  qtopbaslem  22301  tgqioo  22340  cnheiborlem  22489  bndth  22493  fmcfil  22793  ovoliunlem1  22991  volsup  23045  uniioombllem4  23074  uniioombllem5  23075  opnmblALT  23091  volsup2  23093  mbfimaopnlem  23142  mbflimsup  23153  itg2gt0  23247  c1liplem1  23477  dvcnvrelem2  23499  mdegleb  23542  mdeglt  23543  mdegldg  23544  mdegxrcl  23545  mdegcl  23547  ig1peu  23649  efifo  24011  dvlog  24111  efopnlem2  24117  efopn  24118  f1otrg  25466  axcontlem10  25568  eupares  26265  eupath2lem3  26269  htthlem  26961  shsss  27359  imaelshi  28104  pjimai  28222  fimarab  28628  gsummpt2co  28914  sitgclbn  29535  sitgaddlemb  29540  eulerpartlemgvv  29568  eulerpartlemgf  29571  coinfliprv  29674  ballotlemsima  29707  ballotlemro  29714  erdsze2lem2  30243  mrsubrn  30467  msubrn  30483  nocvxminlem  30892  nocvxmin  30893  nobndlem1  30894  nobndlem2  30895  tailf  31343  dissneqlem  32163  poimirlem1  32380  poimirlem2  32381  poimirlem3  32382  poimirlem11  32390  poimirlem12  32391  poimirlem15  32394  poimirlem16  32395  poimirlem19  32398  poimirlem30  32409  itg2addnclem2  32432  itg2gt0cn  32435  ftc1anclem7  32461  ftc1anc  32463  ismtyima  32572  ismtyres  32577  heibor1lem  32578  reheibor  32608  elrfirn  36076  isnacs2  36087  isnacs3  36091  fnwe2lem2  36439  lmhmfgima  36472  brtrclfv2  36838  xphe  36895  imo72b2lem0  37287  imo72b2lem2  37289  imo72b2lem1  37293  imo72b2  37297  limccog  38488  mgmhmima  41591
  Copyright terms: Public domain W3C validator