Theorem imassrn 5940

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 1877	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 3980	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 5932	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5758	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3944	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 399  ∃wex 1787   ∈ wcel 2110  {cab 2714   ⊆ wss 3866  ⟨cop 4547  ran crn 5552   “ cima 5554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-xp 5557  df-cnv 5559  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564

This theorem is referenced by:  0ima  5946  cnvimass  5949  fimass  6566  fimacnvOLD  6891  isofrlem  7149  isofr2  7153  f1opw2  7460  imaexg  7693  f1oweALT  7745  frxp  7893  smores2  8091  ecss  8437  fopwdom  8753  sbthlem2  8757  sbthlem3  8758  sbthlem5  8760  sbthlem6  8761  ssenen  8820  ssfiALT  8852  fiint  8948  f1opwfi  8980  marypha1lem  9049  unxpwdom2  9204  tz9.12lem1  9403  djuin  9534  acndom2  9668  dfac12lem2  9758  isf34lem5  9992  isf34lem7  9993  isf34lem6  9994  enfin1ai  9998  hsmexlem4  10043  hsmexlem5  10044  fpwwe2lem5  10249  fpwwe2lem8  10252  tskuni  10397  limsupgle  15038  limsupval2  15041  limsupgre  15042  isercolllem2  15229  isercoll  15231  unbenlem  16461  imasless  17045  isacs1i  17160  isacs4lem  18050  mhmima  18251  cntzmhm  18733  f1omvdconj  18838  gsumzaddlem  19306  dmdprdd  19386  dprdfeq0  19409  dprdres  19415  dprdss  19416  dprdz  19417  subgdmdprd  19421  dprd2dlem1  19428  dprd2da  19429  dmdprdsplit2lem  19432  lmhmlsp  20086  frlmsslsp  20758  lindff1  20782  lindfrn  20783  f1lindf  20784  lindfmm  20789  lsslindf  20792  cnclsi  22169  cnprest2  22187  paste  22191  cmpfi  22305  connima  22322  1stcfb  22342  1stckgenlem  22450  kgencn3  22455  xkoco1cn  22554  xkoco2cn  22555  xkococnlem  22556  qtopval2  22593  basqtop  22608  imastopn  22617  kqopn  22631  kqcld  22632  hmeontr  22666  hmeores  22668  hmphdis  22693  cmphaushmeo  22697  qtopf1  22713  uzfbas  22795  elfm  22844  elfm3  22847  rnelfm  22850  cnextcn  22964  tgpconncomp  23010  qustgpopn  23017  tsmsf1o  23042  ustimasn  23126  utopbas  23133  restutop  23135  tgqioo  23697  cnheiborlem  23851  bndth  23855  fmcfil  24169  ovoliunlem1  24399  volsup  24453  uniioombllem4  24483  uniioombllem5  24484  opnmblALT  24500  volsup2  24502  mbfimaopnlem  24552  mbflimsup  24563  itg2gt0  24658  c1liplem1  24893  dvcnvrelem2  24915  mdegleb  24962  mdeglt  24963  mdegldg  24964  mdegxrcl  24965  mdegcl  24967  ig1peu  25069  efifo  25436  dvlog  25539  efopnlem2  25545  efopn  25546  f1otrg  26962  axcontlem10  27064  htthlem  28998  shsss  29394  imaelshi  30139  pjimai  30257  gsummpt2co  31027  gsumpart  31034  lsmsnorb  31293  dimkerim  31422  sitgclbn  32022  sitgaddlemb  32027  eulerpartlemgvv  32055  eulerpartlemgf  32058  coinfliprv  32161  ballotlemsima  32194  ballotlemro  32201  erdsze2lem2  32879  mrsubrn  33188  msubrn  33204  frxp2  33528  frxp3  33534  bdayimaon  33633  noetasuplem4  33676  noetainflem4  33680  nocvxminlem  33709  nocvxmin  33710  noeta2  33716  etasslt2  33745  scutbdaybnd2lim  33748  oldf  33778  lrrecfr  33837  tailf  34301  dissneqlem  35248  poimirlem1  35515  poimirlem2  35516  poimirlem3  35517  poimirlem11  35525  poimirlem12  35526  poimirlem15  35529  poimirlem16  35530  poimirlem19  35533  poimirlem30  35544  itg2addnclem2  35566  itg2gt0cn  35569  ftc1anclem7  35593  ftc1anc  35595  ismtyima  35698  ismtyres  35703  heibor1lem  35704  reheibor  35734  imaexALTV  36202  elrfirn  40220  isnacs2  40231  isnacs3  40235  fnwe2lem2  40579  lmhmfgima  40612  brtrclfv2  41012  xphe  41066  imo72b2lem0  41453  imo72b2lem2  41455  imo72b2lem1  41457  imo72b2  41461  limccog  42836  liminfval2  42984  mgmhmima  45029