Theorem imassrn 6068

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 1873	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4062	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6060	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5887	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 4024	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  {cab 2710   ⊆ wss 3947  ⟨cop 4633  ran crn 5676   “ cima 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688

This theorem is referenced by:  0ima  6074  cnvimass  6077  fimass  6735  fimacnvOLD  7068  isofrlem  7332  isofr2  7336  f1opw2  7656  imaexg  7901  f1oweALT  7954  frxp  8107  frxp2  8125  frxp3  8132  smores2  8349  naddunif  8688  naddasslem1  8689  naddasslem2  8690  ecss  8745  fopwdom  9076  sbthlem2  9080  sbthlem3  9081  sbthlem5  9083  sbthlem6  9084  ssenen  9147  ssfiALT  9170  fiint  9320  f1opwfi  9352  marypha1lem  9424  unxpwdom2  9579  tz9.12lem1  9778  djuin  9909  acndom2  10045  dfac12lem2  10135  isf34lem5  10369  isf34lem7  10370  isf34lem6  10371  enfin1ai  10375  hsmexlem4  10420  hsmexlem5  10421  fpwwe2lem5  10626  fpwwe2lem8  10629  tskuni  10774  limsupgle  15417  limsupval2  15420  limsupgre  15421  isercolllem2  15608  isercoll  15610  unbenlem  16837  imasless  17482  isacs1i  17597  isacs4lem  18493  mhmima  18702  cntzmhm  19198  f1omvdconj  19307  gsumzaddlem  19781  dmdprdd  19861  dprdfeq0  19884  dprdres  19890  dprdss  19891  dprdz  19892  subgdmdprd  19896  dprd2dlem1  19903  dprd2da  19904  dmdprdsplit2lem  19907  lmhmlsp  20648  frlmsslsp  21335  lindff1  21359  lindfrn  21360  f1lindf  21361  lindfmm  21366  lsslindf  21369  cnclsi  22758  cnprest2  22776  paste  22780  cmpfi  22894  connima  22911  1stcfb  22931  1stckgenlem  23039  kgencn3  23044  xkoco1cn  23143  xkoco2cn  23144  xkococnlem  23145  qtopval2  23182  basqtop  23197  imastopn  23206  kqopn  23220  kqcld  23221  hmeontr  23255  hmeores  23257  hmphdis  23282  cmphaushmeo  23286  qtopf1  23302  uzfbas  23384  elfm  23433  elfm3  23436  rnelfm  23439  cnextcn  23553  tgpconncomp  23599  qustgpopn  23606  tsmsf1o  23631  ustimasn  23715  utopbas  23722  restutop  23724  tgqioo  24298  cnheiborlem  24452  bndth  24456  fmcfil  24771  ovoliunlem1  25001  volsup  25055  uniioombllem4  25085  uniioombllem5  25086  opnmblALT  25102  volsup2  25104  mbfimaopnlem  25154  mbflimsup  25165  itg2gt0  25260  c1liplem1  25495  dvcnvrelem2  25517  mdegleb  25564  mdeglt  25565  mdegldg  25566  mdegxrcl  25567  mdegcl  25569  ig1peu  25671  efifo  26038  dvlog  26141  efopnlem2  26147  efopn  26148  bdayimaon  27176  noetasuplem4  27219  noetainflem4  27223  nocvxminlem  27259  nocvxmin  27260  noeta2  27266  etasslt2  27295  scutbdaybnd2lim  27298  oldf  27332  lrrecfr  27407  negsunif  27509  negsbdaylem  27510  f1otrg  28102  axcontlem10  28211  htthlem  30148  shsss  30544  imaelshi  31289  pjimai  31407  gsummpt2co  32178  gsumpart  32185  lsmsnorb  32466  dimkerim  32657  sitgclbn  33280  sitgaddlemb  33285  eulerpartlemgvv  33313  eulerpartlemgf  33316  coinfliprv  33419  ballotlemsima  33452  ballotlemro  33459  erdsze2lem2  34133  mrsubrn  34442  msubrn  34458  tailf  35198  dissneqlem  36159  poimirlem1  36427  poimirlem2  36428  poimirlem3  36429  poimirlem11  36437  poimirlem12  36438  poimirlem15  36441  poimirlem16  36442  poimirlem19  36445  poimirlem30  36456  itg2addnclem2  36478  itg2gt0cn  36481  ftc1anclem7  36505  ftc1anc  36507  ismtyima  36609  ismtyres  36614  heibor1lem  36615  reheibor  36645  imaexALTV  37137  elrfirn  41366  isnacs2  41377  isnacs3  41381  fnwe2lem2  41726  lmhmfgima  41759  brtrclfv2  42411  xphe  42465  imo72b2lem0  42850  imo72b2lem2  42852  imo72b2lem1  42854  imo72b2  42857  limccog  44271  liminfval2  44419  mgmhmima  46507