Theorem cnvimass 6039

Description: A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)

Assertion

Ref	Expression
cnvimass	⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Proof of Theorem cnvimass

Step	Hyp	Ref	Expression
1		imassrn 6028	. 2 ⊢ (◡𝐴 “ 𝐵) ⊆ ran ◡𝐴
2		dfdm4 5842	. 2 ⊢ dom 𝐴 = ran ◡𝐴
3	1, 2	sseqtrri 3981	1 ⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Syntax hints:   ⊆ wss 3899  ^◡ccnv 5621  dom cdm 5622  ran crn 5623   “ cima 5625

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 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2713  df-cleq 2726  df-clel 2809  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 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635

This theorem is referenced by:  cnvimassrndm  6108  fvimacnvi  6995  elpreima  7001  cnvimainrn  7010  iinpreima  7012  rescnvimafod  7016  fconst4  7158  fsuppeq  8115  fsuppeqg  8116  pw2f1olem  9007  cnvimamptfin  9251  fisuppfi  9272  infxpenlem  9921  enfin2i  10229  fin1a2lem7  10314  smobeth  10495  fpwwe2lem3  10542  fpwwe2lem11  10550  fpwwe2lem12  10551  fpwwe2  10552  canth4  10556  canthwelem  10559  pwfseqlem4  10571  recmulnq  10873  dmrecnq  10877  ltweuz  13882  isercolllem2  15587  isercolllem3  15588  fsumss  15646  ackbijnn  15749  fprodss  15869  1arith  16853  vdwlem1  16907  vdwlem5  16911  vdwlem6  16912  vdwlem8  16914  vdwlem11  16917  ghmpreima  19165  gicer  19204  torsubg  19781  gsumzmhm  19864  gsumzoppg  19871  lmhmpreima  20998  rhmpreimaidl  21230  evpmss  21539  mplcoe5  21993  psr1baslem  22123  ofco2  22393  cnpnei  23206  cnclima  23210  iscncl  23211  cnntri  23213  cnclsi  23214  cncls2  23215  cncls  23216  cnntr  23217  cncnp  23222  cnrest2  23228  cndis  23233  2ndcomap  23400  kgencn  23498  kgencn3  23500  ptbasfi  23523  txcnmpt  23566  txdis1cn  23577  qtopval2  23638  basqtop  23653  qtopcld  23655  qtopcn  23656  qtopeu  23658  qtoprest  23659  hmeoimaf1o  23712  hmphtop  23720  hmpher  23726  ordthmeolem  23743  elfm3  23892  rnelfmlem  23894  rnelfm  23895  fmfnfmlem2  23897  fmfnfmlem4  23899  clssubg  24051  tgphaus  24059  qustgplem  24063  ucnprima  24223  ucncn  24226  xmeter  24375  imasf1oxms  24431  metustss  24493  metustexhalf  24498  metustfbas  24499  cfilucfil  24501  metuel2  24507  restmetu  24512  mbfconstlem  25582  i1fima  25633  i1fima2  25634  i1fd  25636  itg1addlem5  25655  plyeq0lem  26169  dgrcl  26192  dgrub  26193  dgrlb  26195  vieta1lem1  26272  vieta1lem2  26273  pserulm  26385  psercn2  26386  psercn2OLD  26387  psercnlem2  26388  psercnlem1  26389  psercn  26390  pserdvlem1  26391  pserdvlem2  26392  pserdv  26393  pserdv2  26394  abelth  26405  eff1olem  26511  dvlog  26614  logtayl  26623  cxpcn3lem  26711  cxpcn3  26712  resqrtcn  26713  basellem5  27049  elnlfn  31952  nlelshi  32084  xppreima  32672  ofpreima  32692  ofpreima2  32693  fnpreimac  32698  ffsrn  32756  indpreima  32896  indf1ofs  32897  pwrssmgc  33031  elrgspnsubrunlem2  33279  elrspunidl  33458  ply1degltel  33624  ply1degleel  33625  ply1degltlss  33626  esplysply  33678  dimkerim  33733  lvecendof1f1o  33739  locfinreflem  33946  zarcmplem  33987  carsggect  34424  sibfof  34446  sitgclg  34448  eulerpartlemsv2  34464  eulerpartlemsf  34465  eulerpartlemv  34470  eulerpartlemb  34474  eulerpartlemt  34477  eulerpartlemr  34480  eulerpartlemgu  34483  eulerpartlemgs2  34486  eulerpartlemn  34487  cvmliftmolem1  35424  cvmlift2lem9  35454  cvmlift3lem6  35467  cvmlift3lem7  35468  mthmsta  35721  dvtan  37810  itg2addnclem  37811  ftc1anclem6  37838  sstotbnd2  37914  keridl  38172  diaintclN  41257  dibintclN  41366  dihintcl  41543  pw2f1ocnv  43221  dnnumch3lem  43230  dnnumch3  43231  pwfi2f1o  43280  binomcxplemdvbinom  44536  binomcxplemdvsum  44538  binomcxplemnotnn0  44539  wessf1ornlem  45371  sge0f1o  46568  mbfresmf  46925  smfco  46988  smfsuplem1  46997  fcores  47255  3f1oss1  47263  uniimaprimaeqfv  47570  elsetpreimafvssdm  47574  gricrel  48107  grlicrel  48194