Theorem imassrn 6045

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 1869	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4033	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6037	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5856	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 4001	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  {cab 2708   ⊆ wss 3917  ⟨cop 4598  ran crn 5642   “ cima 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  0ima  6052  cnvimass  6056  f1imadifssran  6605  fimass  6711  isofrlem  7318  isofr2  7322  f1opw2  7647  imaexg  7892  f1oweALT  7954  frxp  8108  frxp2  8126  frxp3  8133  smores2  8326  naddunif  8660  naddasslem1  8661  naddasslem2  8662  ecss  8725  fopwdom  9054  sbthlem2  9058  sbthlem3  9059  sbthlem5  9061  sbthlem6  9062  ssenen  9121  ssfiALT  9144  fiint  9284  fiintOLD  9285  f1opwfi  9314  marypha1lem  9391  unxpwdom2  9548  tz9.12lem1  9747  djuin  9878  acndom2  10014  dfac12lem2  10105  isf34lem5  10338  isf34lem7  10339  isf34lem6  10340  enfin1ai  10344  hsmexlem4  10389  hsmexlem5  10390  fpwwe2lem5  10595  fpwwe2lem8  10598  tskuni  10743  limsupgle  15450  limsupval2  15453  limsupgre  15454  isercolllem2  15639  isercoll  15641  unbenlem  16886  imasless  17510  isacs1i  17625  isacs4lem  18510  mgmhmima  18649  mhmima  18759  cntzmhm  19280  f1omvdconj  19383  gsumzaddlem  19858  dmdprdd  19938  dprdfeq0  19961  dprdres  19967  dprdss  19968  dprdz  19969  subgdmdprd  19973  dprd2dlem1  19980  dprd2da  19981  dmdprdsplit2lem  19984  lmhmlsp  20963  frlmsslsp  21712  lindff1  21736  lindfrn  21737  f1lindf  21738  lindfmm  21743  lsslindf  21746  cnclsi  23166  cnprest2  23184  paste  23188  cmpfi  23302  connima  23319  1stcfb  23339  1stckgenlem  23447  kgencn3  23452  xkoco1cn  23551  xkoco2cn  23552  xkococnlem  23553  qtopval2  23590  basqtop  23605  imastopn  23614  kqopn  23628  kqcld  23629  hmeontr  23663  hmeores  23665  hmphdis  23690  cmphaushmeo  23694  qtopf1  23710  uzfbas  23792  elfm  23841  elfm3  23844  rnelfm  23847  cnextcn  23961  tgpconncomp  24007  qustgpopn  24014  tsmsf1o  24039  ustimasn  24123  utopbas  24130  restutop  24132  tgqioo  24695  cnheiborlem  24860  bndth  24864  fmcfil  25179  ovoliunlem1  25410  volsup  25464  uniioombllem4  25494  uniioombllem5  25495  opnmblALT  25511  volsup2  25513  mbfimaopnlem  25563  mbflimsup  25574  itg2gt0  25668  c1liplem1  25908  dvcnvrelem2  25930  mdegleb  25976  mdeglt  25977  mdegldg  25978  mdegxrcl  25979  mdegcl  25981  ig1peu  26087  efifo  26463  dvlog  26567  efopnlem2  26573  efopn  26574  bdayimaon  27612  noetasuplem4  27655  noetainflem4  27659  nocvxminlem  27696  nocvxmin  27697  noeta2  27703  etasslt2  27733  scutbdaybnd2lim  27736  oldf  27772  lrrecfr  27857  negsunif  27968  negsbdaylem  27969  bdayon  28180  zssno  28276  zs12bday  28350  f1otrg  28805  axcontlem10  28907  htthlem  30853  shsss  31249  imaelshi  31994  pjimai  32112  gsummpt2co  32995  gsumpart  33004  elrgspnsubrunlem2  33206  lsmsnorb  33369  dimkerim  33630  sitgclbn  34341  sitgaddlemb  34346  eulerpartlemgvv  34374  eulerpartlemgf  34377  coinfliprv  34481  ballotlemsima  34514  ballotlemro  34521  onvf1odlem4  35100  erdsze2lem2  35198  mrsubrn  35507  msubrn  35523  tailf  36370  dissneqlem  37335  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem11  37632  poimirlem12  37633  poimirlem15  37636  poimirlem16  37637  poimirlem19  37640  poimirlem30  37651  itg2addnclem2  37673  itg2gt0cn  37676  ftc1anclem7  37700  ftc1anc  37702  ismtyima  37804  ismtyres  37809  heibor1lem  37810  reheibor  37840  elrfirn  42690  isnacs2  42701  isnacs3  42705  fnwe2lem2  43047  lmhmfgima  43080  brtrclfv2  43723  xphe  43777  imo72b2lem2  44163  imo72b2lem1  44165  imo72b2  44168  limccog  45625  liminfval2  45773  imaf1homlem  49100  imaidfu  49103