Theorem imassrn 5824

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 1855	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴) → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴)
2	1	ss2abi 3970	. 2 ⊢ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} ⊆ {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
3		dfima3 5816	. 2 ⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)}
4		dfrn3 5653	. 2 ⊢ ran 𝐴 = {𝑦 ∣ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐴}
5	2, 3, 4	3sstr4i 3937	1 ⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴

Syntax hints:   ∧ wa 396  ∃wex 1765   ∈ wcel 2083  {cab 2777   ⊆ wss 3865  ⟨cop 4484  ran crn 5451   “ cima 5453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969  df-opab 5031  df-xp 5456  df-cnv 5458  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463

This theorem is referenced by:  0ima  5829  cnvimass  5832  fimass  6430  fimacnv  6711  isofrlem  6963  isofr2  6967  f1opw2  7265  imaexg  7483  f1oweALT  7536  frxp  7680  smores2  7850  ecss  8192  fopwdom  8479  sbthlem2  8482  sbthlem3  8483  sbthlem5  8485  sbthlem6  8486  ssenen  8545  ssfi  8591  fiint  8648  f1opwfi  8681  marypha1lem  8750  unxpwdom2  8905  tz9.12lem1  9069  djuin  9200  acndom2  9333  dfac12lem2  9423  isf34lem5  9653  isf34lem7  9654  isf34lem6  9655  enfin1ai  9659  hsmexlem4  9704  hsmexlem5  9705  fpwwe2lem6  9910  fpwwe2lem9  9913  tskuni  10058  limsupgle  14672  limsupval2  14675  limsupgre  14676  isercolllem2  14860  isercoll  14862  unbenlem  16077  imasless  16646  isacs1i  16761  isacs4lem  17611  mhmima  17806  cntzmhm  18214  f1omvdconj  18309  gsumzaddlem  18765  dmdprdd  18842  dprdfeq0  18865  dprdres  18871  dprdss  18872  dprdz  18873  subgdmdprd  18877  dprd2dlem1  18884  dprd2da  18885  dmdprdsplit2lem  18888  lmhmlsp  19515  frlmsslsp  20626  lindff1  20650  lindfrn  20651  f1lindf  20652  lindfmm  20657  lsslindf  20660  cnclsi  21568  cnprest2  21586  paste  21590  cmpfi  21704  connima  21721  1stcfb  21741  1stckgenlem  21849  kgencn3  21854  xkoco1cn  21953  xkoco2cn  21954  xkococnlem  21955  qtopval2  21992  basqtop  22007  imastopn  22016  kqopn  22030  kqcld  22031  hmeontr  22065  hmeores  22067  hmphdis  22092  cmphaushmeo  22096  qtopf1  22112  uzfbas  22194  elfm  22243  elfm3  22246  rnelfm  22249  cnextcn  22363  tgpconncomp  22408  qustgpopn  22415  tsmsf1o  22440  ustimasn  22524  utopbas  22531  restutop  22533  tgqioo  23095  cnheiborlem  23245  bndth  23249  fmcfil  23562  ovoliunlem1  23790  volsup  23844  uniioombllem4  23874  uniioombllem5  23875  opnmblALT  23891  volsup2  23893  mbfimaopnlem  23943  mbflimsup  23954  itg2gt0  24048  c1liplem1  24280  dvcnvrelem2  24302  mdegleb  24345  mdeglt  24346  mdegldg  24347  mdegxrcl  24348  mdegcl  24350  ig1peu  24452  efifo  24816  dvlog  24919  efopnlem2  24925  efopn  24926  f1otrg  26344  axcontlem10  26446  htthlem  28381  shsss  28777  imaelshi  29522  pjimai  29640  gsummpt2co  30491  dimkerim  30623  sitgclbn  31214  sitgaddlemb  31219  eulerpartlemgvv  31247  eulerpartlemgf  31250  coinfliprv  31353  ballotlemsima  31386  ballotlemro  31393  erdsze2lem2  32061  mrsubrn  32370  msubrn  32386  bdayimaon  32808  nosupbday  32816  noetalem3  32830  noetalem4  32831  nocvxminlem  32858  nocvxmin  32859  tailf  33334  dissneqlem  34173  poimirlem1  34445  poimirlem2  34446  poimirlem3  34447  poimirlem11  34455  poimirlem12  34456  poimirlem15  34459  poimirlem16  34460  poimirlem19  34463  poimirlem30  34474  itg2addnclem2  34496  itg2gt0cn  34499  ftc1anclem7  34525  ftc1anc  34527  ismtyima  34634  ismtyres  34639  heibor1lem  34640  reheibor  34670  imaexALTV  35140  elrfirn  38798  isnacs2  38809  isnacs3  38813  fnwe2lem2  39157  lmhmfgima  39190  brtrclfv2  39578  xphe  39633  imo72b2lem0  40022  imo72b2lem2  40024  imo72b2lem1  40028  imo72b2  40032  limccog  41464  liminfval2  41612  mgmhmima  43573