Theorem imassrn 6026

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.

Step	Hyp	Ref	Expression
1		exsimpr 1869	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4021	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6018	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5836	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3989	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  {cab 2707   ⊆ wss 3905  ⟨cop 4585  ran crn 5624   “ cima 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636

This theorem is referenced by:  0ima  6033  cnvimass  6037  f1imadifssran  6572  fimass  6676  isofrlem  7281  isofr2  7285  f1opw2  7608  imaexg  7853  f1oweALT  7914  frxp  8066  frxp2  8084  frxp3  8091  smores2  8284  naddunif  8618  naddasslem1  8619  naddasslem2  8620  ecss  8683  fopwdom  9009  sbthlem2  9012  sbthlem3  9013  sbthlem5  9015  sbthlem6  9016  ssenen  9075  ssfiALT  9098  fiint  9235  fiintOLD  9236  f1opwfi  9265  marypha1lem  9342  unxpwdom2  9499  tz9.12lem1  9702  djuin  9833  acndom2  9967  dfac12lem2  10058  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  enfin1ai  10297  hsmexlem4  10342  hsmexlem5  10343  fpwwe2lem5  10548  fpwwe2lem8  10551  tskuni  10696  limsupgle  15402  limsupval2  15405  limsupgre  15406  isercolllem2  15591  isercoll  15593  unbenlem  16838  imasless  17462  isacs1i  17581  isacs4lem  18468  mgmhmima  18607  mhmima  18717  cntzmhm  19238  f1omvdconj  19343  gsumzaddlem  19818  dmdprdd  19898  dprdfeq0  19921  dprdres  19927  dprdss  19928  dprdz  19929  subgdmdprd  19933  dprd2dlem1  19940  dprd2da  19941  dmdprdsplit2lem  19944  lmhmlsp  20971  frlmsslsp  21721  lindff1  21745  lindfrn  21746  f1lindf  21747  lindfmm  21752  lsslindf  21755  cnclsi  23175  cnprest2  23193  paste  23197  cmpfi  23311  connima  23328  1stcfb  23348  1stckgenlem  23456  kgencn3  23461  xkoco1cn  23560  xkoco2cn  23561  xkococnlem  23562  qtopval2  23599  basqtop  23614  imastopn  23623  kqopn  23637  kqcld  23638  hmeontr  23672  hmeores  23674  hmphdis  23699  cmphaushmeo  23703  qtopf1  23719  uzfbas  23801  elfm  23850  elfm3  23853  rnelfm  23856  cnextcn  23970  tgpconncomp  24016  qustgpopn  24023  tsmsf1o  24048  ustimasn  24132  utopbas  24139  restutop  24141  tgqioo  24704  cnheiborlem  24869  bndth  24873  fmcfil  25188  ovoliunlem1  25419  volsup  25473  uniioombllem4  25503  uniioombllem5  25504  opnmblALT  25520  volsup2  25522  mbfimaopnlem  25572  mbflimsup  25583  itg2gt0  25677  c1liplem1  25917  dvcnvrelem2  25939  mdegleb  25985  mdeglt  25986  mdegldg  25987  mdegxrcl  25988  mdegcl  25990  ig1peu  26096  efifo  26472  dvlog  26576  efopnlem2  26582  efopn  26583  bdayimaon  27621  noetasuplem4  27664  noetainflem4  27668  nobdaymin  27705  nocvxminlem  27706  noeta2  27713  etasslt2  27743  scutbdaybnd2lim  27746  oldf  27785  lrrecfr  27873  negsunif  27984  negsbdaylem  27985  bdayon  28196  zssno  28292  zs12bday  28379  f1otrg  28834  axcontlem10  28936  htthlem  30879  shsss  31275  imaelshi  32020  pjimai  32138  gsummpt2co  33014  gsumpart  33023  elrgspnsubrunlem2  33201  lsmsnorb  33341  dimkerim  33602  sitgclbn  34313  sitgaddlemb  34318  eulerpartlemgvv  34346  eulerpartlemgf  34349  coinfliprv  34453  ballotlemsima  34486  ballotlemro  34493  onvf1odlem4  35081  erdsze2lem2  35179  mrsubrn  35488  msubrn  35504  tailf  36351  dissneqlem  37316  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem11  37613  poimirlem12  37614  poimirlem15  37617  poimirlem16  37618  poimirlem19  37621  poimirlem30  37632  itg2addnclem2  37654  itg2gt0cn  37657  ftc1anclem7  37681  ftc1anc  37683  ismtyima  37785  ismtyres  37790  heibor1lem  37791  reheibor  37821  elrfirn  42671  isnacs2  42682  isnacs3  42686  fnwe2lem2  43027  lmhmfgima  43060  brtrclfv2  43703  xphe  43757  imo72b2lem2  44143  imo72b2lem1  44145  imo72b2  44148  limccog  45605  liminfval2  45753  imaf1homlem  49096  imaidfu  49099