Theorem imassrn 5942

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

Syntax hints:   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  {cab 2801   ⊆ wss 3938  ⟨cop 4575  ran crn 5558   “ cima 5560

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570

This theorem is referenced by:  0ima  5948  cnvimass  5951  fimass  6557  fimacnv  6841  isofrlem  7095  isofr2  7099  f1opw2  7402  imaexg  7622  f1oweALT  7675  frxp  7822  smores2  7993  ecss  8337  fopwdom  8627  sbthlem2  8630  sbthlem3  8631  sbthlem5  8633  sbthlem6  8634  ssenen  8693  ssfi  8740  fiint  8797  f1opwfi  8830  marypha1lem  8899  unxpwdom2  9054  tz9.12lem1  9218  djuin  9349  acndom2  9482  dfac12lem2  9572  isf34lem5  9802  isf34lem7  9803  isf34lem6  9804  enfin1ai  9808  hsmexlem4  9853  hsmexlem5  9854  fpwwe2lem6  10059  fpwwe2lem9  10062  tskuni  10207  limsupgle  14836  limsupval2  14839  limsupgre  14840  isercolllem2  15024  isercoll  15026  unbenlem  16246  imasless  16815  isacs1i  16930  isacs4lem  17780  mhmima  17991  cntzmhm  18471  f1omvdconj  18576  gsumzaddlem  19043  dmdprdd  19123  dprdfeq0  19146  dprdres  19152  dprdss  19153  dprdz  19154  subgdmdprd  19158  dprd2dlem1  19165  dprd2da  19166  dmdprdsplit2lem  19169  lmhmlsp  19823  frlmsslsp  20942  lindff1  20966  lindfrn  20967  f1lindf  20968  lindfmm  20973  lsslindf  20976  cnclsi  21882  cnprest2  21900  paste  21904  cmpfi  22018  connima  22035  1stcfb  22055  1stckgenlem  22163  kgencn3  22168  xkoco1cn  22267  xkoco2cn  22268  xkococnlem  22269  qtopval2  22306  basqtop  22321  imastopn  22330  kqopn  22344  kqcld  22345  hmeontr  22379  hmeores  22381  hmphdis  22406  cmphaushmeo  22410  qtopf1  22426  uzfbas  22508  elfm  22557  elfm3  22560  rnelfm  22563  cnextcn  22677  tgpconncomp  22723  qustgpopn  22730  tsmsf1o  22755  ustimasn  22839  utopbas  22846  restutop  22848  tgqioo  23410  cnheiborlem  23560  bndth  23564  fmcfil  23877  ovoliunlem1  24105  volsup  24159  uniioombllem4  24189  uniioombllem5  24190  opnmblALT  24206  volsup2  24208  mbfimaopnlem  24258  mbflimsup  24269  itg2gt0  24363  c1liplem1  24595  dvcnvrelem2  24617  mdegleb  24660  mdeglt  24661  mdegldg  24662  mdegxrcl  24663  mdegcl  24665  ig1peu  24767  efifo  25133  dvlog  25236  efopnlem2  25242  efopn  25243  f1otrg  26659  axcontlem10  26761  htthlem  28696  shsss  29092  imaelshi  29837  pjimai  29955  gsummpt2co  30688  lsmsnorb  30947  dimkerim  31025  sitgclbn  31603  sitgaddlemb  31608  eulerpartlemgvv  31636  eulerpartlemgf  31639  coinfliprv  31742  ballotlemsima  31775  ballotlemro  31782  erdsze2lem2  32453  mrsubrn  32762  msubrn  32778  bdayimaon  33199  nosupbday  33207  noetalem3  33221  noetalem4  33222  nocvxminlem  33249  nocvxmin  33250  tailf  33725  dissneqlem  34623  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem11  34905  poimirlem12  34906  poimirlem15  34909  poimirlem16  34910  poimirlem19  34913  poimirlem30  34924  itg2addnclem2  34946  itg2gt0cn  34949  ftc1anclem7  34975  ftc1anc  34977  ismtyima  35083  ismtyres  35088  heibor1lem  35089  reheibor  35119  imaexALTV  35589  elrfirn  39299  isnacs2  39310  isnacs3  39314  fnwe2lem2  39658  lmhmfgima  39691  brtrclfv2  40079  xphe  40134  imo72b2lem0  40523  imo72b2lem2  40525  imo72b2lem1  40528  imo72b2  40532  limccog  41908  liminfval2  42056  mgmhmima  44076