Theorem imassrn 6075

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 1899	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4021	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6067	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5881	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3989	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 400  ∃wex 1809   ∈ wcel 2143  {cab 2741   ⊆ wss 3906  ⟨cop 4596  ran crn 5664   “ cima 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is referenced by:  0ima  6082  cnvimass  6086  fimass  6728  isofrlem  7340  isofr2  7344  f1opw2  7667  imaexg  7911  f1oweALT  7970  frxp  8123  frxp2  8141  frxp3  8148  smores2  8342  naddunif  8681  naddasslem1  8682  naddasslem2  8683  ecss  8747  fopwdom  9074  sbthlem2  9077  sbthlem3  9078  sbthlem5  9080  sbthlem6  9081  ssenen  9140  ssfiALT  9159  fiint  9287  f1opwfi  9314  marypha1lem  9394  unxpwdom2  9551  tz9.12lem1  9760  djuin  9905  acndom2  10039  dfac12lem2  10129  isf34lem5  10363  isf34lem7  10364  isf34lem6  10365  enfin1ai  10369  hsmexlem4  10414  hsmexlem5  10415  fpwwe2lem5  10621  fpwwe2lem8  10624  tskuni  10769  limsupgle  15530  limsupval2  15533  limsupgre  15534  isercolllem2  15719  isercoll  15721  unbenlem  16969  imasless  17595  isacs1i  17714  isacs4lem  18601  mgmhmima  18774  mhmima  18885  cntzmhm  19412  f1omvdconj  19517  gsumzaddlem  19992  dmdprdd  20072  dprdfeq0  20095  dprdres  20101  dprdss  20102  dprdz  20103  subgdmdprd  20107  dprd2dlem1  20114  dprd2da  20115  dmdprdsplit2lem  20118  lmhmlsp  21151  frlmsslsp  21927  lindff1  21951  lindfrn  21952  f1lindf  21953  lindfmm  21958  lsslindf  21961  cnclsi  23410  cnprest2  23428  paste  23432  cmpfi  23546  connima  23563  1stcfb  23583  1stckgenlem  23691  kgencn3  23696  xkoco1cn  23795  xkoco2cn  23796  xkococnlem  23797  qtopval2  23834  basqtop  23849  imastopn  23858  kqopn  23872  kqcld  23873  hmeontr  23907  hmeores  23909  hmphdis  23934  cmphaushmeo  23938  qtopf1  23954  uzfbas  24036  elfm  24085  elfm3  24088  rnelfm  24091  cnextcn  24205  tgpconncomp  24251  qustgpopn  24258  tsmsf1o  24283  ustimasn  24366  utopbas  24373  restutop  24375  tgqioo  24938  cnheiborlem  25094  bndth  25098  fmcfil  25412  ovoliunlem1  25642  volsup  25696  uniioombllem4  25726  uniioombllem5  25727  opnmblALT  25743  volsup2  25745  mbfimaopnlem  25795  mbflimsup  25806  itg2gt0  25900  c1liplem1  26136  dvcnvrelem2  26158  mdegleb  26202  mdeglt  26203  mdegldg  26204  mdegxrcl  26205  mdegcl  26207  ig1peu  26313  efifo  26693  dvlog  26797  efopnlem2  26803  efopn  26804  bdayimaon  27838  noetasuplem4  27881  noetainflem4  27885  nobdaymin  27927  nocvxminlem  27928  noeta2  27935  etaslts2  27968  cutbdaybnd2lim  27971  oldf  28011  lrrecfr  28117  negsunif  28229  negbdaylem  28230  bdayons  28450  zssno  28555  f1otrg  29201  axcontlem10  29304  htthlem  31250  shsss  31646  imaelshi  32391  pjimai  32509  gsummpt2co  33349  gsumpart  33364  elrgspnsubrunlem2  33549  lsmsnorb  33685  dimkerim  33998  sitgclbn  34714  sitgaddlemb  34719  eulerpartlemgvv  34747  eulerpartlemgf  34750  coinfliprv  34854  ballotlemsima  34887  ballotlemro  34894  onvf1odlem4  35571  erdsze2lem2  35677  mrsubrn  35986  msubrn  36002  tailf  36867  dissneqlem  37967  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem11  38263  poimirlem12  38264  poimirlem15  38267  poimirlem16  38268  poimirlem19  38271  poimirlem30  38282  itg2addnclem2  38304  itg2gt0cn  38307  ftc1anclem7  38331  ftc1anc  38333  ismtyima  38435  ismtyres  38440  heibor1lem  38441  reheibor  38471  elrfirn  43409  isnacs2  43420  isnacs3  43424  fnwe2lem2  43761  lmhmfgima  43794  brtrclfv2  44436  xphe  44490  imo72b2lem2  44876  imo72b2lem1  44878  imo72b2  44881  limccog  46319  liminfval2  46465  imaf1homlem  49868  imaidfu  49871