Theorem cnvimass 6101

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 6090	. 2 ⊢ (◡𝐴 “ 𝐵) ⊆ ran ◡𝐴
2		dfdm4 5908	. 2 ⊢ dom 𝐴 = ran ◡𝐴
3	1, 2	sseqtrri 4032	1 ⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Syntax hints:   ⊆ wss 3962  ^◡ccnv 5687  dom cdm 5688  ran crn 5689   “ cima 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701

This theorem is referenced by:  cnvimassrndm  6173  fvimacnvi  7071  elpreima  7077  cnvimainrn  7086  iinpreima  7088  rescnvimafod  7092  fconst4  7233  fsuppeq  8198  fsuppeqg  8199  pw2f1olem  9114  cnvimamptfin  9390  fisuppfi  9408  infxpenlem  10050  enfin2i  10358  fin1a2lem7  10443  smobeth  10623  fpwwe2lem3  10670  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  canth4  10684  canthwelem  10687  pwfseqlem4  10699  recmulnq  11001  dmrecnq  11005  ltweuz  13998  isercolllem2  15698  isercolllem3  15699  fsumss  15757  ackbijnn  15860  fprodss  15980  1arith  16960  vdwlem1  17014  vdwlem5  17018  vdwlem6  17019  vdwlem8  17021  vdwlem11  17024  ghmpreima  19268  gicer  19307  torsubg  19886  gsumzmhm  19969  gsumzoppg  19976  lmhmpreima  21064  rhmpreimaidl  21304  evpmss  21621  mplcoe5  22075  psr1baslem  22201  ofco2  22472  cnpnei  23287  cnclima  23291  iscncl  23292  cnntri  23294  cnclsi  23295  cncls2  23296  cncls  23297  cnntr  23298  cncnp  23303  cnrest2  23309  cndis  23314  2ndcomap  23481  kgencn  23579  kgencn3  23581  ptbasfi  23604  txcnmpt  23647  txdis1cn  23658  qtopval2  23719  basqtop  23734  qtopcld  23736  qtopcn  23737  qtopeu  23739  qtoprest  23740  hmeoimaf1o  23793  hmphtop  23801  hmpher  23807  ordthmeolem  23824  elfm3  23973  rnelfmlem  23975  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem4  23980  clssubg  24132  tgphaus  24140  qustgplem  24144  ucnprima  24306  ucncn  24309  xmeter  24458  imasf1oxms  24517  metustss  24579  metustexhalf  24584  metustfbas  24585  cfilucfil  24587  metuel2  24593  restmetu  24598  mbfconstlem  25675  i1fima  25726  i1fima2  25727  i1fd  25729  itg1addlem5  25749  plyeq0lem  26263  dgrcl  26286  dgrub  26287  dgrlb  26289  vieta1lem1  26366  vieta1lem2  26367  pserulm  26479  psercn2  26480  psercn2OLD  26481  psercnlem2  26482  psercnlem1  26483  psercn  26484  pserdvlem1  26485  pserdvlem2  26486  pserdv  26487  pserdv2  26488  abelth  26499  eff1olem  26604  dvlog  26707  logtayl  26716  cxpcn3lem  26804  cxpcn3  26805  resqrtcn  26806  basellem5  27142  elnlfn  31956  nlelshi  32088  xppreima  32661  ofpreima  32681  ofpreima2  32682  fnpreimac  32687  ffsrn  32746  pwrssmgc  32974  elrspunidl  33435  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  dimkerim  33654  lvecendof1f1o  33660  locfinreflem  33800  zarcmplem  33841  indpreima  34005  indf1ofs  34006  carsggect  34299  sibfof  34321  sitgclg  34323  eulerpartlemsv2  34339  eulerpartlemsf  34340  eulerpartlemv  34345  eulerpartlemb  34349  eulerpartlemt  34352  eulerpartlemr  34355  eulerpartlemgu  34358  eulerpartlemgs2  34361  eulerpartlemn  34362  cvmliftmolem1  35265  cvmlift2lem9  35295  cvmlift3lem6  35308  cvmlift3lem7  35309  mthmsta  35562  dvtan  37656  itg2addnclem  37657  ftc1anclem6  37684  sstotbnd2  37760  keridl  38018  diaintclN  41040  dibintclN  41149  dihintcl  41326  pw2f1ocnv  43025  dnnumch3lem  43034  dnnumch3  43035  pwfi2f1o  43084  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  wessf1ornlem  45127  sge0f1o  46337  mbfresmf  46694  smfco  46757  smfsuplem1  46766  fcores  47016  3f1oss1  47024  uniimaprimaeqfv  47306  elsetpreimafvssdm  47310  gricrel  47825  grlicrel  47901