Theorem imassrn 6078

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 1902	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4023	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6070	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5884	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3991	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812   ∈ wcel 2146  {cab 2744   ⊆ wss 3908  ⟨cop 4600  ran crn 5667   “ cima 5669

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-cnv 5674  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679

This theorem is used by:  0ima  6085  cnvimass  6089  fimass  6733  isofrlem  7349  isofr2  7353  f1opw2  7678  imaexg  7919  f1oweALT  7978  frxp  8131  frxp2  8149  frxp3  8156  smores2  8350  naddunif  8689  naddasslem1  8690  naddasslem2  8691  ecss  8755  fopwdom  9083  sbthlem2  9086  sbthlem3  9087  sbthlem5  9089  sbthlem6  9090  ssenen  9149  ssfiALT  9168  fiint  9296  f1opwfi  9323  marypha1lem  9403  unxpwdom2  9560  tz9.12lem1  9769  djuin  9923  acndom2  10057  dfac12lem2  10147  isf34lem5  10380  isf34lem7  10381  isf34lem6  10382  enfin1ai  10386  hsmexlem4  10431  hsmexlem5  10432  fpwwe2lem5  10638  fpwwe2lem8  10641  tskuni  10786  limsupgle  15554  limsupval2  15557  limsupgre  15558  isercolllem2  15743  isercoll  15745  unbenlem  16993  imasless  17619  isacs1i  17738  isacs4lem  18625  mgmhmima  18802  mhmima  18915  cntzmhm  19442  f1omvdconj  19547  gsumzaddlem  20022  dmdprdd  20102  dprdfeq0  20125  dprdres  20131  dprdss  20132  dprdz  20133  subgdmdprd  20137  dprd2dlem1  20144  dprd2da  20145  dmdprdsplit2lem  20148  lmhmlsp  21207  frlmsslsp  21983  lindff1  22007  lindfrn  22008  f1lindf  22009  lindfmm  22014  lsslindf  22017  cnclsi  23466  cnprest2  23484  paste  23488  cmpfi  23602  connima  23619  1stcfb  23639  1stckgenlem  23747  kgencn3  23752  xkoco1cn  23851  xkoco2cn  23852  xkococnlem  23853  qtopval2  23890  basqtop  23905  imastopn  23914  kqopn  23928  kqcld  23929  hmeontr  23963  hmeores  23965  hmphdis  23990  cmphaushmeo  23994  qtopf1  24010  uzfbas  24092  elfm  24141  elfm3  24144  rnelfm  24147  cnextcn  24261  tgpconncomp  24307  qustgpopn  24314  tsmsf1o  24339  ustimasn  24422  utopbas  24429  restutop  24431  tgqioo  24994  cnheiborlem  25150  bndth  25154  fmcfil  25468  ovoliunlem1  25698  volsup  25752  uniioombllem4  25782  uniioombllem5  25783  opnmblALT  25799  volsup2  25801  mbfimaopnlem  25851  mbflimsup  25862  itg2gt0  25956  c1liplem1  26192  dvcnvrelem2  26214  mdegleb  26258  mdeglt  26259  mdegldg  26260  mdegxrcl  26261  mdegcl  26263  ig1peu  26369  efifo  26749  dvlog  26853  efopnlem2  26859  efopn  26860  bdayimaon  27894  noetasuplem4  27937  noetainflem4  27941  nobdaymin  27983  nocvxminlem  27984  noeta2  27991  etaslts2  28024  cutbdaybnd2lim  28027  oldf  28067  lrrecfr  28173  negsunif  28285  negbdaylem  28286  bdayons  28506  zssno  28611  f1otrg  29257  axcontlem10  29360  htthlem  31306  shsss  31702  imaelshi  32447  pjimai  32565  gsummpt2co  33399  gsumpart  33414  elrgspnsubrunlem2  33599  lsmsnorb  33735  dimkerim  34048  sitgclbn  34765  sitgaddlemb  34770  eulerpartlemgvv  34798  eulerpartlemgf  34801  coinfliprv  34905  ballotlemsima  34938  ballotlemro  34945  onvf1odlem4  35614  erdsze2lem2  35717  mrsubrn  36026  msubrn  36042  tailf  36927  dissneqlem  38027  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem11  38323  poimirlem12  38324  poimirlem15  38327  poimirlem16  38328  poimirlem19  38331  poimirlem30  38342  itg2addnclem2  38364  itg2gt0cn  38367  ftc1anclem7  38391  ftc1anc  38393  ismtyima  38495  ismtyres  38500  heibor1lem  38501  reheibor  38531  elrfirn  43467  isnacs2  43478  isnacs3  43482  fnwe2lem2  43819  lmhmfgima  43852  brtrclfv2  44494  xphe  44548  imo72b2lem2  44934  imo72b2lem1  44936  imo72b2  44939  limccog  46377  liminfval2  46523  imaf1homlem  49926  imaidfu  49929