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

Theorem imassrn 5908
 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 1870 . . 3 (∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴)
21ss2abi 3994 . 2 {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
3 dfima3 5900 . 2 (𝐴𝐵) = {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4 dfrn3 5725 . 2 ran 𝐴 = {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
52, 3, 43sstr4i 3958 1 (𝐴𝐵) ⊆ ran 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  {cab 2776   ⊆ wss 3881  ⟨cop 4531  ran crn 5521   “ cima 5523 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pr 5296 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5032  df-opab 5094  df-xp 5526  df-cnv 5528  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533 This theorem is referenced by:  0ima  5914  cnvimass  5917  fimass  6530  fimacnv  6817  isofrlem  7073  isofr2  7077  f1opw2  7382  imaexg  7605  f1oweALT  7658  frxp  7806  smores2  7977  ecss  8321  fopwdom  8611  sbthlem2  8615  sbthlem3  8616  sbthlem5  8618  sbthlem6  8619  ssenen  8678  ssfi  8725  fiint  8782  f1opwfi  8815  marypha1lem  8884  unxpwdom2  9039  tz9.12lem1  9203  djuin  9334  acndom2  9468  dfac12lem2  9558  isf34lem5  9792  isf34lem7  9793  isf34lem6  9794  enfin1ai  9798  hsmexlem4  9843  hsmexlem5  9844  fpwwe2lem5  10049  fpwwe2lem8  10052  tskuni  10197  limsupgle  14829  limsupval2  14832  limsupgre  14833  isercolllem2  15017  isercoll  15019  unbenlem  16237  imasless  16808  isacs1i  16923  isacs4lem  17773  mhmima  17984  cntzmhm  18465  f1omvdconj  18570  gsumzaddlem  19038  dmdprdd  19118  dprdfeq0  19141  dprdres  19147  dprdss  19148  dprdz  19149  subgdmdprd  19153  dprd2dlem1  19160  dprd2da  19161  dmdprdsplit2lem  19164  lmhmlsp  19818  frlmsslsp  20490  lindff1  20514  lindfrn  20515  f1lindf  20516  lindfmm  20521  lsslindf  20524  cnclsi  21887  cnprest2  21905  paste  21909  cmpfi  22023  connima  22040  1stcfb  22060  1stckgenlem  22168  kgencn3  22173  xkoco1cn  22272  xkoco2cn  22273  xkococnlem  22274  qtopval2  22311  basqtop  22326  imastopn  22335  kqopn  22349  kqcld  22350  hmeontr  22384  hmeores  22386  hmphdis  22411  cmphaushmeo  22415  qtopf1  22431  uzfbas  22513  elfm  22562  elfm3  22565  rnelfm  22568  cnextcn  22682  tgpconncomp  22728  qustgpopn  22735  tsmsf1o  22760  ustimasn  22844  utopbas  22851  restutop  22853  tgqioo  23415  cnheiborlem  23569  bndth  23573  fmcfil  23886  ovoliunlem1  24116  volsup  24170  uniioombllem4  24200  uniioombllem5  24201  opnmblALT  24217  volsup2  24219  mbfimaopnlem  24269  mbflimsup  24280  itg2gt0  24374  c1liplem1  24609  dvcnvrelem2  24631  mdegleb  24675  mdeglt  24676  mdegldg  24677  mdegxrcl  24678  mdegcl  24680  ig1peu  24782  efifo  25149  dvlog  25252  efopnlem2  25258  efopn  25259  f1otrg  26675  axcontlem10  26777  htthlem  28710  shsss  29106  imaelshi  29851  pjimai  29969  gsummpt2co  30743  gsumpart  30750  lsmsnorb  31009  dimkerim  31126  sitgclbn  31726  sitgaddlemb  31731  eulerpartlemgvv  31759  eulerpartlemgf  31762  coinfliprv  31865  ballotlemsima  31898  ballotlemro  31905  erdsze2lem2  32579  mrsubrn  32888  msubrn  32904  bdayimaon  33325  nosupbday  33333  noetalem3  33347  noetalem4  33348  nocvxminlem  33375  nocvxmin  33376  tailf  33851  dissneqlem  34776  poimirlem1  35077  poimirlem2  35078  poimirlem3  35079  poimirlem11  35087  poimirlem12  35088  poimirlem15  35091  poimirlem16  35092  poimirlem19  35095  poimirlem30  35106  itg2addnclem2  35128  itg2gt0cn  35131  ftc1anclem7  35155  ftc1anc  35157  ismtyima  35260  ismtyres  35265  heibor1lem  35266  reheibor  35296  imaexALTV  35766  elrfirn  39679  isnacs2  39690  isnacs3  39694  fnwe2lem2  40038  lmhmfgima  40071  brtrclfv2  40471  xphe  40525  imo72b2lem0  40912  imo72b2lem2  40914  imo72b2lem1  40917  imo72b2  40921  limccog  42305  liminfval2  42453  mgmhmima  44465
 Copyright terms: Public domain W3C validator