Theorem imassrn 6069

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

Syntax hints:   ∧ wa 394  ∃wex 1779   ∈ wcel 2104  {cab 2707   ⊆ wss 3947  ⟨cop 4633  ran crn 5676   “ cima 5678

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688

This theorem is referenced by:  0ima  6076  cnvimass  6079  fimass  6737  fimacnvOLD  7071  isofrlem  7339  isofr2  7343  f1opw2  7663  imaexg  7908  f1oweALT  7961  frxp  8114  frxp2  8132  frxp3  8139  smores2  8356  naddunif  8694  naddasslem1  8695  naddasslem2  8696  ecss  8751  fopwdom  9082  sbthlem2  9086  sbthlem3  9087  sbthlem5  9089  sbthlem6  9090  ssenen  9153  ssfiALT  9176  fiint  9326  f1opwfi  9358  marypha1lem  9430  unxpwdom2  9585  tz9.12lem1  9784  djuin  9915  acndom2  10051  dfac12lem2  10141  isf34lem5  10375  isf34lem7  10376  isf34lem6  10377  enfin1ai  10381  hsmexlem4  10426  hsmexlem5  10427  fpwwe2lem5  10632  fpwwe2lem8  10635  tskuni  10780  limsupgle  15425  limsupval2  15428  limsupgre  15429  isercolllem2  15616  isercoll  15618  unbenlem  16845  imasless  17490  isacs1i  17605  isacs4lem  18501  mgmhmima  18640  mhmima  18742  cntzmhm  19246  f1omvdconj  19355  gsumzaddlem  19830  dmdprdd  19910  dprdfeq0  19933  dprdres  19939  dprdss  19940  dprdz  19941  subgdmdprd  19945  dprd2dlem1  19952  dprd2da  19953  dmdprdsplit2lem  19956  lmhmlsp  20804  frlmsslsp  21570  lindff1  21594  lindfrn  21595  f1lindf  21596  lindfmm  21601  lsslindf  21604  cnclsi  22996  cnprest2  23014  paste  23018  cmpfi  23132  connima  23149  1stcfb  23169  1stckgenlem  23277  kgencn3  23282  xkoco1cn  23381  xkoco2cn  23382  xkococnlem  23383  qtopval2  23420  basqtop  23435  imastopn  23444  kqopn  23458  kqcld  23459  hmeontr  23493  hmeores  23495  hmphdis  23520  cmphaushmeo  23524  qtopf1  23540  uzfbas  23622  elfm  23671  elfm3  23674  rnelfm  23677  cnextcn  23791  tgpconncomp  23837  qustgpopn  23844  tsmsf1o  23869  ustimasn  23953  utopbas  23960  restutop  23962  tgqioo  24536  cnheiborlem  24700  bndth  24704  fmcfil  25020  ovoliunlem1  25251  volsup  25305  uniioombllem4  25335  uniioombllem5  25336  opnmblALT  25352  volsup2  25354  mbfimaopnlem  25404  mbflimsup  25415  itg2gt0  25510  c1liplem1  25748  dvcnvrelem2  25770  mdegleb  25817  mdeglt  25818  mdegldg  25819  mdegxrcl  25820  mdegcl  25822  ig1peu  25924  efifo  26292  dvlog  26395  efopnlem2  26401  efopn  26402  bdayimaon  27432  noetasuplem4  27475  noetainflem4  27479  nocvxminlem  27515  nocvxmin  27516  noeta2  27522  etasslt2  27552  scutbdaybnd2lim  27555  oldf  27589  lrrecfr  27665  negsunif  27768  negsbdaylem  27769  f1otrg  28389  axcontlem10  28498  htthlem  30437  shsss  30833  imaelshi  31578  pjimai  31696  gsummpt2co  32470  gsumpart  32477  lsmsnorb  32775  dimkerim  33000  sitgclbn  33640  sitgaddlemb  33645  eulerpartlemgvv  33673  eulerpartlemgf  33676  coinfliprv  33779  ballotlemsima  33812  ballotlemro  33819  erdsze2lem2  34493  mrsubrn  34802  msubrn  34818  tailf  35563  dissneqlem  36524  poimirlem1  36792  poimirlem2  36793  poimirlem3  36794  poimirlem11  36802  poimirlem12  36803  poimirlem15  36806  poimirlem16  36807  poimirlem19  36810  poimirlem30  36821  itg2addnclem2  36843  itg2gt0cn  36846  ftc1anclem7  36870  ftc1anc  36872  ismtyima  36974  ismtyres  36979  heibor1lem  36980  reheibor  37010  imaexALTV  37502  elrfirn  41735  isnacs2  41746  isnacs3  41750  fnwe2lem2  42095  lmhmfgima  42128  brtrclfv2  42780  xphe  42834  imo72b2lem0  43219  imo72b2lem2  43221  imo72b2lem1  43223  imo72b2  43226  limccog  44634  liminfval2  44782