Theorem imassrn 6100

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 1868	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 4090	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 6092	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5914	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 4052	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  {cab 2717   ⊆ wss 3976  ⟨cop 4654  ran crn 5701   “ cima 5703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713

This theorem is referenced by:  0ima  6107  cnvimass  6111  fimass  6767  fimacnvOLD  7104  isofrlem  7376  isofr2  7380  f1opw2  7705  imaexg  7953  f1oweALT  8013  frxp  8167  frxp2  8185  frxp3  8192  smores2  8410  naddunif  8749  naddasslem1  8750  naddasslem2  8751  ecss  8811  fopwdom  9146  sbthlem2  9150  sbthlem3  9151  sbthlem5  9153  sbthlem6  9154  ssenen  9217  ssfiALT  9241  fiint  9394  fiintOLD  9395  f1opwfi  9426  marypha1lem  9502  unxpwdom2  9657  tz9.12lem1  9856  djuin  9987  acndom2  10123  dfac12lem2  10214  isf34lem5  10447  isf34lem7  10448  isf34lem6  10449  enfin1ai  10453  hsmexlem4  10498  hsmexlem5  10499  fpwwe2lem5  10704  fpwwe2lem8  10707  tskuni  10852  limsupgle  15523  limsupval2  15526  limsupgre  15527  isercolllem2  15714  isercoll  15716  unbenlem  16955  imasless  17600  isacs1i  17715  isacs4lem  18614  mgmhmima  18753  mhmima  18860  cntzmhm  19381  f1omvdconj  19488  gsumzaddlem  19963  dmdprdd  20043  dprdfeq0  20066  dprdres  20072  dprdss  20073  dprdz  20074  subgdmdprd  20078  dprd2dlem1  20085  dprd2da  20086  dmdprdsplit2lem  20089  lmhmlsp  21071  frlmsslsp  21839  lindff1  21863  lindfrn  21864  f1lindf  21865  lindfmm  21870  lsslindf  21873  cnclsi  23301  cnprest2  23319  paste  23323  cmpfi  23437  connima  23454  1stcfb  23474  1stckgenlem  23582  kgencn3  23587  xkoco1cn  23686  xkoco2cn  23687  xkococnlem  23688  qtopval2  23725  basqtop  23740  imastopn  23749  kqopn  23763  kqcld  23764  hmeontr  23798  hmeores  23800  hmphdis  23825  cmphaushmeo  23829  qtopf1  23845  uzfbas  23927  elfm  23976  elfm3  23979  rnelfm  23982  cnextcn  24096  tgpconncomp  24142  qustgpopn  24149  tsmsf1o  24174  ustimasn  24258  utopbas  24265  restutop  24267  tgqioo  24841  cnheiborlem  25005  bndth  25009  fmcfil  25325  ovoliunlem1  25556  volsup  25610  uniioombllem4  25640  uniioombllem5  25641  opnmblALT  25657  volsup2  25659  mbfimaopnlem  25709  mbflimsup  25720  itg2gt0  25815  c1liplem1  26055  dvcnvrelem2  26077  mdegleb  26123  mdeglt  26124  mdegldg  26125  mdegxrcl  26126  mdegcl  26128  ig1peu  26234  efifo  26607  dvlog  26711  efopnlem2  26717  efopn  26718  bdayimaon  27756  noetasuplem4  27799  noetainflem4  27803  nocvxminlem  27840  nocvxmin  27841  noeta2  27847  etasslt2  27877  scutbdaybnd2lim  27880  oldf  27914  lrrecfr  27994  negsunif  28105  negsbdaylem  28106  zssno  28385  zs12bday  28442  f1otrg  28897  axcontlem10  29006  htthlem  30949  shsss  31345  imaelshi  32090  pjimai  32208  gsummpt2co  33031  gsumpart  33038  lsmsnorb  33384  dimkerim  33640  sitgclbn  34308  sitgaddlemb  34313  eulerpartlemgvv  34341  eulerpartlemgf  34344  coinfliprv  34447  ballotlemsima  34480  ballotlemro  34487  erdsze2lem2  35172  mrsubrn  35481  msubrn  35497  tailf  36341  dissneqlem  37306  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem11  37591  poimirlem12  37592  poimirlem15  37595  poimirlem16  37596  poimirlem19  37599  poimirlem30  37610  itg2addnclem2  37632  itg2gt0cn  37635  ftc1anclem7  37659  ftc1anc  37661  ismtyima  37763  ismtyres  37768  heibor1lem  37769  reheibor  37799  imaexALTV  38286  elrfirn  42651  isnacs2  42662  isnacs3  42666  fnwe2lem2  43008  lmhmfgima  43041  brtrclfv2  43689  xphe  43743  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2lem1  44131  imo72b2  44134  limccog  45541  liminfval2  45689