Theorem imassrn 6027

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 1870	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4016	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6019	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5836	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3983	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  {cab 2711   ⊆ wss 3899  ⟨cop 4583  ran crn 5622   “ cima 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634

This theorem is referenced by:  0ima  6034  cnvimass  6038  f1imadifssran  6575  fimass  6679  isofrlem  7283  isofr2  7287  f1opw2  7610  imaexg  7852  f1oweALT  7913  frxp  8065  frxp2  8083  frxp3  8090  smores2  8283  naddunif  8617  naddasslem1  8618  naddasslem2  8619  ecss  8682  fopwdom  9008  sbthlem2  9011  sbthlem3  9012  sbthlem5  9014  sbthlem6  9015  ssenen  9074  ssfiALT  9093  fiint  9221  f1opwfi  9250  marypha1lem  9327  unxpwdom2  9484  tz9.12lem1  9690  djuin  9821  acndom2  9955  dfac12lem2  10046  isf34lem5  10279  isf34lem7  10280  isf34lem6  10281  enfin1ai  10285  hsmexlem4  10330  hsmexlem5  10331  fpwwe2lem5  10536  fpwwe2lem8  10539  tskuni  10684  limsupgle  15394  limsupval2  15397  limsupgre  15398  isercolllem2  15583  isercoll  15585  unbenlem  16830  imasless  17454  isacs1i  17573  isacs4lem  18460  mgmhmima  18633  mhmima  18743  cntzmhm  19263  f1omvdconj  19368  gsumzaddlem  19843  dmdprdd  19923  dprdfeq0  19946  dprdres  19952  dprdss  19953  dprdz  19954  subgdmdprd  19958  dprd2dlem1  19965  dprd2da  19966  dmdprdsplit2lem  19969  lmhmlsp  20993  frlmsslsp  21743  lindff1  21767  lindfrn  21768  f1lindf  21769  lindfmm  21774  lsslindf  21777  cnclsi  23197  cnprest2  23215  paste  23219  cmpfi  23333  connima  23350  1stcfb  23370  1stckgenlem  23478  kgencn3  23483  xkoco1cn  23582  xkoco2cn  23583  xkococnlem  23584  qtopval2  23621  basqtop  23636  imastopn  23645  kqopn  23659  kqcld  23660  hmeontr  23694  hmeores  23696  hmphdis  23721  cmphaushmeo  23725  qtopf1  23741  uzfbas  23823  elfm  23872  elfm3  23875  rnelfm  23878  cnextcn  23992  tgpconncomp  24038  qustgpopn  24045  tsmsf1o  24070  ustimasn  24153  utopbas  24160  restutop  24162  tgqioo  24725  cnheiborlem  24890  bndth  24894  fmcfil  25209  ovoliunlem1  25440  volsup  25494  uniioombllem4  25524  uniioombllem5  25525  opnmblALT  25541  volsup2  25543  mbfimaopnlem  25593  mbflimsup  25604  itg2gt0  25698  c1liplem1  25938  dvcnvrelem2  25960  mdegleb  26006  mdeglt  26007  mdegldg  26008  mdegxrcl  26009  mdegcl  26011  ig1peu  26117  efifo  26493  dvlog  26597  efopnlem2  26603  efopn  26604  bdayimaon  27642  noetasuplem4  27685  noetainflem4  27689  nobdaymin  27726  nocvxminlem  27727  noeta2  27734  etasslt2  27765  scutbdaybnd2lim  27768  oldf  27808  lrrecfr  27896  negsunif  28007  negsbdaylem  28008  bdayon  28219  zssno  28315  zs12bday  28404  f1otrg  28859  axcontlem10  28962  htthlem  30908  shsss  31304  imaelshi  32049  pjimai  32167  gsummpt2co  33039  gsumpart  33048  elrgspnsubrunlem2  33226  lsmsnorb  33367  dimkerim  33651  sitgclbn  34367  sitgaddlemb  34372  eulerpartlemgvv  34400  eulerpartlemgf  34403  coinfliprv  34507  ballotlemsima  34540  ballotlemro  34547  onvf1odlem4  35161  erdsze2lem2  35259  mrsubrn  35568  msubrn  35584  tailf  36430  dissneqlem  37395  poimirlem1  37671  poimirlem2  37672  poimirlem3  37673  poimirlem11  37681  poimirlem12  37682  poimirlem15  37685  poimirlem16  37686  poimirlem19  37689  poimirlem30  37700  itg2addnclem2  37722  itg2gt0cn  37725  ftc1anclem7  37749  ftc1anc  37751  ismtyima  37853  ismtyres  37858  heibor1lem  37859  reheibor  37889  elrfirn  42802  isnacs2  42813  isnacs3  42817  fnwe2lem2  43158  lmhmfgima  43191  brtrclfv2  43834  xphe  43888  imo72b2lem2  44274  imo72b2lem1  44276  imo72b2  44279  limccog  45734  liminfval2  45880  imaf1homlem  49222  imaidfu  49225