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

Theorem imassrn 5933
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 4040 . 2 {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
3 dfima3 5925 . 2 (𝐴𝐵) = {𝑦 ∣ ∃𝑥(𝑥𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4 dfrn3 5753 . 2 ran 𝐴 = {𝑦 ∣ ∃𝑥𝑥, 𝑦⟩ ∈ 𝐴}
52, 3, 43sstr4i 4007 1 (𝐴𝐵) ⊆ ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 396  wex 1771  wcel 2105  {cab 2796  wss 3933  cop 4563  ran crn 5549  cima 5551
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 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
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 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-xp 5554  df-cnv 5556  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561
This theorem is referenced by:  0ima  5939  cnvimass  5942  fimass  6548  fimacnv  6831  isofrlem  7082  isofr2  7086  f1opw2  7389  imaexg  7609  f1oweALT  7662  frxp  7809  smores2  7980  ecss  8324  fopwdom  8613  sbthlem2  8616  sbthlem3  8617  sbthlem5  8619  sbthlem6  8620  ssenen  8679  ssfi  8726  fiint  8783  f1opwfi  8816  marypha1lem  8885  unxpwdom2  9040  tz9.12lem1  9204  djuin  9335  acndom2  9468  dfac12lem2  9558  isf34lem5  9788  isf34lem7  9789  isf34lem6  9790  enfin1ai  9794  hsmexlem4  9839  hsmexlem5  9840  fpwwe2lem6  10045  fpwwe2lem9  10048  tskuni  10193  limsupgle  14822  limsupval2  14825  limsupgre  14826  isercolllem2  15010  isercoll  15012  unbenlem  16232  imasless  16801  isacs1i  16916  isacs4lem  17766  mhmima  17977  cntzmhm  18407  f1omvdconj  18503  gsumzaddlem  18970  dmdprdd  19050  dprdfeq0  19073  dprdres  19079  dprdss  19080  dprdz  19081  subgdmdprd  19085  dprd2dlem1  19092  dprd2da  19093  dmdprdsplit2lem  19096  lmhmlsp  19750  frlmsslsp  20868  lindff1  20892  lindfrn  20893  f1lindf  20894  lindfmm  20899  lsslindf  20902  cnclsi  21808  cnprest2  21826  paste  21830  cmpfi  21944  connima  21961  1stcfb  21981  1stckgenlem  22089  kgencn3  22094  xkoco1cn  22193  xkoco2cn  22194  xkococnlem  22195  qtopval2  22232  basqtop  22247  imastopn  22256  kqopn  22270  kqcld  22271  hmeontr  22305  hmeores  22307  hmphdis  22332  cmphaushmeo  22336  qtopf1  22352  uzfbas  22434  elfm  22483  elfm3  22486  rnelfm  22489  cnextcn  22603  tgpconncomp  22648  qustgpopn  22655  tsmsf1o  22680  ustimasn  22764  utopbas  22771  restutop  22773  tgqioo  23335  cnheiborlem  23485  bndth  23489  fmcfil  23802  ovoliunlem1  24030  volsup  24084  uniioombllem4  24114  uniioombllem5  24115  opnmblALT  24131  volsup2  24133  mbfimaopnlem  24183  mbflimsup  24194  itg2gt0  24288  c1liplem1  24520  dvcnvrelem2  24542  mdegleb  24585  mdeglt  24586  mdegldg  24587  mdegxrcl  24588  mdegcl  24590  ig1peu  24692  efifo  25058  dvlog  25161  efopnlem2  25167  efopn  25168  f1otrg  26584  axcontlem10  26686  htthlem  28621  shsss  29017  imaelshi  29762  pjimai  29880  gsummpt2co  30613  dimkerim  30922  sitgclbn  31500  sitgaddlemb  31505  eulerpartlemgvv  31533  eulerpartlemgf  31536  coinfliprv  31639  ballotlemsima  31672  ballotlemro  31679  erdsze2lem2  32348  mrsubrn  32657  msubrn  32673  bdayimaon  33094  nosupbday  33102  noetalem3  33116  noetalem4  33117  nocvxminlem  33144  nocvxmin  33145  tailf  33620  dissneqlem  34503  poimirlem1  34774  poimirlem2  34775  poimirlem3  34776  poimirlem11  34784  poimirlem12  34785  poimirlem15  34788  poimirlem16  34789  poimirlem19  34792  poimirlem30  34803  itg2addnclem2  34825  itg2gt0cn  34828  ftc1anclem7  34854  ftc1anc  34856  ismtyima  34962  ismtyres  34967  heibor1lem  34968  reheibor  34998  imaexALTV  35468  elrfirn  39170  isnacs2  39181  isnacs3  39185  fnwe2lem2  39529  lmhmfgima  39562  brtrclfv2  39950  xphe  40005  imo72b2lem0  40394  imo72b2lem2  40396  imo72b2lem1  40399  imo72b2  40403  limccog  41777  liminfval2  41925  mgmhmima  43946
  Copyright terms: Public domain W3C validator