Theorem imassrn 6071

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 4064	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6063	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5890	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 4026	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

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

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 5300  ax-nul 5307  ax-pr 5428

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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690

This theorem is referenced by:  0ima  6078  cnvimass  6081  fimass  6739  fimacnvOLD  7073  isofrlem  7337  isofr2  7341  f1opw2  7661  imaexg  7906  f1oweALT  7959  frxp  8112  frxp2  8130  frxp3  8137  smores2  8354  naddunif  8692  naddasslem1  8693  naddasslem2  8694  ecss  8749  fopwdom  9080  sbthlem2  9084  sbthlem3  9085  sbthlem5  9087  sbthlem6  9088  ssenen  9151  ssfiALT  9174  fiint  9324  f1opwfi  9356  marypha1lem  9428  unxpwdom2  9583  tz9.12lem1  9782  djuin  9913  acndom2  10049  dfac12lem2  10139  isf34lem5  10373  isf34lem7  10374  isf34lem6  10375  enfin1ai  10379  hsmexlem4  10424  hsmexlem5  10425  fpwwe2lem5  10630  fpwwe2lem8  10633  tskuni  10778  limsupgle  15421  limsupval2  15424  limsupgre  15425  isercolllem2  15612  isercoll  15614  unbenlem  16841  imasless  17486  isacs1i  17601  isacs4lem  18497  mhmima  18706  cntzmhm  19205  f1omvdconj  19314  gsumzaddlem  19789  dmdprdd  19869  dprdfeq0  19892  dprdres  19898  dprdss  19899  dprdz  19900  subgdmdprd  19904  dprd2dlem1  19911  dprd2da  19912  dmdprdsplit2lem  19915  lmhmlsp  20660  frlmsslsp  21351  lindff1  21375  lindfrn  21376  f1lindf  21377  lindfmm  21382  lsslindf  21385  cnclsi  22776  cnprest2  22794  paste  22798  cmpfi  22912  connima  22929  1stcfb  22949  1stckgenlem  23057  kgencn3  23062  xkoco1cn  23161  xkoco2cn  23162  xkococnlem  23163  qtopval2  23200  basqtop  23215  imastopn  23224  kqopn  23238  kqcld  23239  hmeontr  23273  hmeores  23275  hmphdis  23300  cmphaushmeo  23304  qtopf1  23320  uzfbas  23402  elfm  23451  elfm3  23454  rnelfm  23457  cnextcn  23571  tgpconncomp  23617  qustgpopn  23624  tsmsf1o  23649  ustimasn  23733  utopbas  23740  restutop  23742  tgqioo  24316  cnheiborlem  24470  bndth  24474  fmcfil  24789  ovoliunlem1  25019  volsup  25073  uniioombllem4  25103  uniioombllem5  25104  opnmblALT  25120  volsup2  25122  mbfimaopnlem  25172  mbflimsup  25183  itg2gt0  25278  c1liplem1  25513  dvcnvrelem2  25535  mdegleb  25582  mdeglt  25583  mdegldg  25584  mdegxrcl  25585  mdegcl  25587  ig1peu  25689  efifo  26056  dvlog  26159  efopnlem2  26165  efopn  26166  bdayimaon  27196  noetasuplem4  27239  noetainflem4  27243  nocvxminlem  27279  nocvxmin  27280  noeta2  27286  etasslt2  27315  scutbdaybnd2lim  27318  oldf  27352  lrrecfr  27427  negsunif  27529  negsbdaylem  27530  f1otrg  28122  axcontlem10  28231  htthlem  30170  shsss  30566  imaelshi  31311  pjimai  31429  gsummpt2co  32200  gsumpart  32207  lsmsnorb  32501  dimkerim  32712  sitgclbn  33342  sitgaddlemb  33347  eulerpartlemgvv  33375  eulerpartlemgf  33378  coinfliprv  33481  ballotlemsima  33514  ballotlemro  33521  erdsze2lem2  34195  mrsubrn  34504  msubrn  34520  tailf  35260  dissneqlem  36221  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem11  36499  poimirlem12  36500  poimirlem15  36503  poimirlem16  36504  poimirlem19  36507  poimirlem30  36518  itg2addnclem2  36540  itg2gt0cn  36543  ftc1anclem7  36567  ftc1anc  36569  ismtyima  36671  ismtyres  36676  heibor1lem  36677  reheibor  36707  imaexALTV  37199  elrfirn  41433  isnacs2  41444  isnacs3  41448  fnwe2lem2  41793  lmhmfgima  41826  brtrclfv2  42478  xphe  42532  imo72b2lem0  42917  imo72b2lem2  42919  imo72b2lem1  42921  imo72b2  42924  limccog  44336  liminfval2  44484  mgmhmima  46572