Theorem imassrn 6030

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 1876	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4004	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6022	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5838	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3973	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  {cab 2718   ⊆ wss 3890  ⟨cop 4568  ran crn 5626   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  0ima  6037  cnvimass  6041  f1imadifssran  6578  fimass  6682  isofrlem  7291  isofr2  7295  f1opw2  7618  imaexg  7860  f1oweALT  7921  frxp  8073  frxp2  8091  frxp3  8098  smores2  8291  naddunif  8626  naddasslem1  8627  naddasslem2  8628  ecss  8692  fopwdom  9020  sbthlem2  9023  sbthlem3  9024  sbthlem5  9026  sbthlem6  9027  ssenen  9086  ssfiALT  9105  fiint  9234  f1opwfi  9263  marypha1lem  9343  unxpwdom2  9500  tz9.12lem1  9709  djuin  9840  acndom2  9974  dfac12lem2  10065  isf34lem5  10298  isf34lem7  10299  isf34lem6  10300  enfin1ai  10304  hsmexlem4  10349  hsmexlem5  10350  fpwwe2lem5  10556  fpwwe2lem8  10559  tskuni  10704  limsupgle  15437  limsupval2  15440  limsupgre  15441  isercolllem2  15626  isercoll  15628  unbenlem  16877  imasless  17502  isacs1i  17621  isacs4lem  18508  mgmhmima  18681  mhmima  18791  cntzmhm  19314  f1omvdconj  19419  gsumzaddlem  19894  dmdprdd  19974  dprdfeq0  19997  dprdres  20003  dprdss  20004  dprdz  20005  subgdmdprd  20009  dprd2dlem1  20016  dprd2da  20017  dmdprdsplit2lem  20020  lmhmlsp  21046  frlmsslsp  21778  lindff1  21802  lindfrn  21803  f1lindf  21804  lindfmm  21809  lsslindf  21812  cnclsi  23262  cnprest2  23280  paste  23284  cmpfi  23398  connima  23415  1stcfb  23435  1stckgenlem  23543  kgencn3  23548  xkoco1cn  23647  xkoco2cn  23648  xkococnlem  23649  qtopval2  23686  basqtop  23701  imastopn  23710  kqopn  23724  kqcld  23725  hmeontr  23759  hmeores  23761  hmphdis  23786  cmphaushmeo  23790  qtopf1  23806  uzfbas  23888  elfm  23937  elfm3  23940  rnelfm  23943  cnextcn  24057  tgpconncomp  24103  qustgpopn  24110  tsmsf1o  24135  ustimasn  24218  utopbas  24225  restutop  24227  tgqioo  24790  cnheiborlem  24946  bndth  24950  fmcfil  25264  ovoliunlem1  25494  volsup  25548  uniioombllem4  25578  uniioombllem5  25579  opnmblALT  25595  volsup2  25597  mbfimaopnlem  25647  mbflimsup  25658  itg2gt0  25752  c1liplem1  25988  dvcnvrelem2  26010  mdegleb  26054  mdeglt  26055  mdegldg  26056  mdegxrcl  26057  mdegcl  26059  ig1peu  26165  efifo  26536  dvlog  26640  efopnlem2  26646  efopn  26647  bdayimaon  27682  noetasuplem4  27725  noetainflem4  27729  nobdaymin  27770  nocvxminlem  27771  noeta2  27778  etaslts2  27811  cutbdaybnd2lim  27814  oldf  27854  lrrecfr  27960  negsunif  28072  negbdaylem  28073  bdayons  28293  zssno  28398  f1otrg  28964  axcontlem10  29067  htthlem  31013  shsss  31409  imaelshi  32154  pjimai  32272  gsummpt2co  33136  gsumpart  33151  elrgspnsubrunlem2  33336  lsmsnorb  33481  dimkerim  33818  sitgclbn  34534  sitgaddlemb  34539  eulerpartlemgvv  34567  eulerpartlemgf  34570  coinfliprv  34674  ballotlemsima  34707  ballotlemro  34714  onvf1odlem4  35341  erdsze2lem2  35439  mrsubrn  35748  msubrn  35764  tailf  36610  dissneqlem  37709  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem11  38005  poimirlem12  38006  poimirlem15  38009  poimirlem16  38010  poimirlem19  38013  poimirlem30  38024  itg2addnclem2  38046  itg2gt0cn  38049  ftc1anclem7  38073  ftc1anc  38075  ismtyima  38177  ismtyres  38182  heibor1lem  38183  reheibor  38213  elrfirn  43151  isnacs2  43162  isnacs3  43166  fnwe2lem2  43503  lmhmfgima  43536  brtrclfv2  44178  xphe  44232  imo72b2lem2  44618  imo72b2lem1  44620  imo72b2  44623  limccog  46072  liminfval2  46218  imaf1homlem  49604  imaidfu  49607