Theorem cnvimass 6043

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

Syntax hints:   ⊆ wss 3890  ^◡ccnv 5625  dom cdm 5626  ran crn 5627   “ cima 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5632  df-cnv 5634  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639

This theorem is referenced by:  cnvimassrndm  6112  fvimacnvi  7000  elpreima  7006  cnvimainrn  7015  iinpreima  7017  rescnvimafod  7021  fconst4  7164  fsuppeq  8120  fsuppeqg  8121  pw2f1olem  9014  cnvimamptfin  9258  fisuppfi  9279  infxpenlem  9930  enfin2i  10238  fin1a2lem7  10323  smobeth  10504  fpwwe2lem3  10551  fpwwe2lem11  10559  fpwwe2lem12  10560  fpwwe2  10561  canth4  10565  canthwelem  10568  pwfseqlem4  10580  recmulnq  10882  dmrecnq  10886  ltweuz  13918  isercolllem2  15623  isercolllem3  15624  fsumss  15682  ackbijnn  15788  fprodss  15908  1arith  16893  vdwlem1  16947  vdwlem5  16951  vdwlem6  16952  vdwlem8  16954  vdwlem11  16957  ghmpreima  19208  gicer  19247  torsubg  19824  gsumzmhm  19907  gsumzoppg  19914  lmhmpreima  21039  rhmpreimaidl  21271  evpmss  21580  mplcoe5  22032  psr1baslem  22162  ofco2  22430  cnpnei  23243  cnclima  23247  iscncl  23248  cnntri  23250  cnclsi  23251  cncls2  23252  cncls  23253  cnntr  23254  cncnp  23259  cnrest2  23265  cndis  23270  2ndcomap  23437  kgencn  23535  kgencn3  23537  ptbasfi  23560  txcnmpt  23603  txdis1cn  23614  qtopval2  23675  basqtop  23690  qtopcld  23692  qtopcn  23693  qtopeu  23695  qtoprest  23696  hmeoimaf1o  23749  hmphtop  23757  hmpher  23763  ordthmeolem  23780  elfm3  23929  rnelfmlem  23931  rnelfm  23932  fmfnfmlem2  23934  fmfnfmlem4  23936  clssubg  24088  tgphaus  24096  qustgplem  24100  ucnprima  24260  ucncn  24263  xmeter  24412  imasf1oxms  24468  metustss  24530  metustexhalf  24535  metustfbas  24536  cfilucfil  24538  metuel2  24544  restmetu  24549  mbfconstlem  25608  i1fima  25659  i1fima2  25660  i1fd  25662  itg1addlem5  25681  plyeq0lem  26189  dgrcl  26212  dgrub  26213  dgrlb  26215  vieta1lem1  26291  vieta1lem2  26292  pserulm  26404  psercn2  26405  psercnlem2  26406  psercnlem1  26407  psercn  26408  pserdvlem1  26409  pserdvlem2  26410  pserdv  26411  pserdv2  26412  abelth  26423  eff1olem  26529  dvlog  26632  logtayl  26641  cxpcn3lem  26728  cxpcn3  26729  resqrtcn  26730  basellem5  27066  elnlfn  32018  nlelshi  32150  xppreima  32737  ofpreima  32757  ofpreima2  32758  fnpreimac  32762  ffsrn  32820  indpreima  32944  indf1ofs  32945  pwrssmgc  33079  elrgspnsubrunlem2  33328  elrspunidl  33507  ply1degltel  33673  ply1degleel  33674  ply1degltlss  33675  esplysply  33734  dimkerim  33791  lvecendof1f1o  33797  locfinreflem  34004  zarcmplem  34045  carsggect  34482  sibfof  34504  sitgclg  34506  eulerpartlemsv2  34522  eulerpartlemsf  34523  eulerpartlemv  34528  eulerpartlemb  34532  eulerpartlemt  34535  eulerpartlemr  34538  eulerpartlemgu  34541  eulerpartlemgs2  34544  eulerpartlemn  34545  cvmliftmolem1  35483  cvmlift2lem9  35513  cvmlift3lem6  35526  cvmlift3lem7  35527  mthmsta  35780  dvtan  38009  itg2addnclem  38010  ftc1anclem6  38037  sstotbnd2  38113  keridl  38371  diaintclN  41522  dibintclN  41631  dihintcl  41808  pw2f1ocnv  43487  dnnumch3lem  43496  dnnumch3  43497  pwfi2f1o  43546  binomcxplemdvbinom  44802  binomcxplemdvsum  44804  binomcxplemnotnn0  44805  wessf1ornlem  45637  sge0f1o  46832  mbfresmf  47189  smfco  47252  smfsuplem1  47261  fcores  47531  3f1oss1  47539  uniimaprimaeqfv  47858  elsetpreimafvssdm  47862  gricrel  48411  grlicrel  48498