Theorem imassrn 6024

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 1870	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4015	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6016	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5833	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3982	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  {cab 2711   ⊆ wss 3898  ⟨cop 4581  ran crn 5620   “ cima 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  0ima  6031  cnvimass  6035  f1imadifssran  6572  fimass  6676  isofrlem  7280  isofr2  7284  f1opw2  7607  imaexg  7849  f1oweALT  7910  frxp  8062  frxp2  8080  frxp3  8087  smores2  8280  naddunif  8614  naddasslem1  8615  naddasslem2  8616  ecss  8679  fopwdom  9005  sbthlem2  9008  sbthlem3  9009  sbthlem5  9011  sbthlem6  9012  ssenen  9071  ssfiALT  9090  fiint  9218  f1opwfi  9247  marypha1lem  9324  unxpwdom2  9481  tz9.12lem1  9687  djuin  9818  acndom2  9952  dfac12lem2  10043  isf34lem5  10276  isf34lem7  10277  isf34lem6  10278  enfin1ai  10282  hsmexlem4  10327  hsmexlem5  10328  fpwwe2lem5  10533  fpwwe2lem8  10536  tskuni  10681  limsupgle  15386  limsupval2  15389  limsupgre  15390  isercolllem2  15575  isercoll  15577  unbenlem  16822  imasless  17446  isacs1i  17565  isacs4lem  18452  mgmhmima  18625  mhmima  18735  cntzmhm  19255  f1omvdconj  19360  gsumzaddlem  19835  dmdprdd  19915  dprdfeq0  19938  dprdres  19944  dprdss  19945  dprdz  19946  subgdmdprd  19950  dprd2dlem1  19957  dprd2da  19958  dmdprdsplit2lem  19961  lmhmlsp  20985  frlmsslsp  21735  lindff1  21759  lindfrn  21760  f1lindf  21761  lindfmm  21766  lsslindf  21769  cnclsi  23188  cnprest2  23206  paste  23210  cmpfi  23324  connima  23341  1stcfb  23361  1stckgenlem  23469  kgencn3  23474  xkoco1cn  23573  xkoco2cn  23574  xkococnlem  23575  qtopval2  23612  basqtop  23627  imastopn  23636  kqopn  23650  kqcld  23651  hmeontr  23685  hmeores  23687  hmphdis  23712  cmphaushmeo  23716  qtopf1  23732  uzfbas  23814  elfm  23863  elfm3  23866  rnelfm  23869  cnextcn  23983  tgpconncomp  24029  qustgpopn  24036  tsmsf1o  24061  ustimasn  24144  utopbas  24151  restutop  24153  tgqioo  24716  cnheiborlem  24881  bndth  24885  fmcfil  25200  ovoliunlem1  25431  volsup  25485  uniioombllem4  25515  uniioombllem5  25516  opnmblALT  25532  volsup2  25534  mbfimaopnlem  25584  mbflimsup  25595  itg2gt0  25689  c1liplem1  25929  dvcnvrelem2  25951  mdegleb  25997  mdeglt  25998  mdegldg  25999  mdegxrcl  26000  mdegcl  26002  ig1peu  26108  efifo  26484  dvlog  26588  efopnlem2  26594  efopn  26595  bdayimaon  27633  noetasuplem4  27676  noetainflem4  27680  nobdaymin  27717  nocvxminlem  27718  noeta2  27725  etasslt2  27756  scutbdaybnd2lim  27759  oldf  27799  lrrecfr  27887  negsunif  27998  negsbdaylem  27999  bdayon  28210  zssno  28306  zs12bday  28395  f1otrg  28850  axcontlem10  28953  htthlem  30899  shsss  31295  imaelshi  32040  pjimai  32158  gsummpt2co  33035  gsumpart  33044  elrgspnsubrunlem2  33222  lsmsnorb  33363  dimkerim  33661  sitgclbn  34377  sitgaddlemb  34382  eulerpartlemgvv  34410  eulerpartlemgf  34413  coinfliprv  34517  ballotlemsima  34550  ballotlemro  34557  onvf1odlem4  35171  erdsze2lem2  35269  mrsubrn  35578  msubrn  35594  tailf  36440  dissneqlem  37405  poimirlem1  37682  poimirlem2  37683  poimirlem3  37684  poimirlem11  37692  poimirlem12  37693  poimirlem15  37696  poimirlem16  37697  poimirlem19  37700  poimirlem30  37711  itg2addnclem2  37733  itg2gt0cn  37736  ftc1anclem7  37760  ftc1anc  37762  ismtyima  37864  ismtyres  37869  heibor1lem  37870  reheibor  37900  elrfirn  42813  isnacs2  42824  isnacs3  42828  fnwe2lem2  43169  lmhmfgima  43202  brtrclfv2  43845  xphe  43899  imo72b2lem2  44285  imo72b2lem1  44287  imo72b2  44290  limccog  45745  liminfval2  45891  imaf1homlem  49233  imaidfu  49236