Theorem cnvimass 6041

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

Syntax hints:   ⊆ wss 3885  ^◡ccnv 5620  dom cdm 5621  ran crn 5622   “ cima 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-xp 5627  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634

This theorem is referenced by:  cnvimassrndm  6107  fvimacnvi  6997  elpreima  7003  cnvimainrn  7012  iinpreima  7014  rescnvimafod  7018  fconst4  7162  fsuppeq  8119  fsuppeqg  8120  pw2f1olem  9013  cnvimamptfin  9257  fisuppfi  9278  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  21042  rhmpreimaidl  21274  evpmss  21565  mplcoe5  22020  psr1baslem  22174  ofco2  22438  cnpnei  23251  cnclima  23255  iscncl  23256  cnntri  23258  cnclsi  23259  cncls2  23260  cncls  23261  cnntr  23262  cncnp  23267  cnrest2  23273  cndis  23278  2ndcomap  23445  kgencn  23543  kgencn3  23545  ptbasfi  23568  txcnmpt  23611  txdis1cn  23622  qtopval2  23683  basqtop  23698  qtopcld  23700  qtopcn  23701  qtopeu  23703  qtoprest  23704  hmeoimaf1o  23757  hmphtop  23765  hmpher  23771  ordthmeolem  23788  elfm3  23937  rnelfmlem  23939  rnelfm  23940  fmfnfmlem2  23942  fmfnfmlem4  23944  clssubg  24096  tgphaus  24104  qustgplem  24108  ucnprima  24268  ucncn  24271  xmeter  24420  imasf1oxms  24476  metustss  24538  metustexhalf  24543  metustfbas  24544  cfilucfil  24546  metuel2  24552  restmetu  24557  mbfconstlem  25616  i1fima  25667  i1fima2  25668  i1fd  25670  itg1addlem5  25689  plyeq0lem  26197  dgrcl  26220  dgrub  26221  dgrlb  26223  vieta1lem1  26298  vieta1lem2  26299  pserulm  26409  psercn2  26410  psercnlem2  26411  psercnlem1  26412  psercn  26413  pserdvlem1  26414  pserdvlem2  26415  pserdv  26416  pserdv2  26417  abelth  26428  eff1olem  26534  dvlog  26637  logtayl  26646  cxpcn3lem  26733  cxpcn3  26734  resqrtcn  26735  basellem5  27070  elnlfn  32021  nlelshi  32153  xppreima  32741  ofpreima  32761  ofpreima2  32762  fnpreimac  32766  ffsrn  32824  indpreima  32948  indf1ofs  32949  pwrssmgc  33083  elrgspnsubrunlem2  33333  elrspunidl  33515  ply1degltel  33689  ply1degleel  33690  ply1degltlss  33691  esplysply  33767  dimkerim  33823  lvecendof1f1o  33829  locfinreflem  34036  zarcmplem  34077  carsggect  34514  sibfof  34536  sitgclg  34538  eulerpartlemsv2  34554  eulerpartlemsf  34555  eulerpartlemv  34560  eulerpartlemb  34564  eulerpartlemt  34567  eulerpartlemr  34570  eulerpartlemgu  34573  eulerpartlemgs2  34576  eulerpartlemn  34577  cvmliftmolem1  35524  cvmlift2lem9  35554  cvmlift3lem6  35567  cvmlift3lem7  35568  mthmsta  35821  dvtan  38052  itg2addnclem  38053  ftc1anclem6  38080  sstotbnd2  38156  keridl  38414  diaintclN  41565  dibintclN  41674  dihintcl  41851  pw2f1ocnv  43497  dnnumch3lem  43506  dnnumch3  43507  pwfi2f1o  43556  binomcxplemdvbinom  44812  binomcxplemdvsum  44814  binomcxplemnotnn0  44815  wessf1ornlem  45646  sge0f1o  46839  mbfresmf  47196  smfco  47259  smfsuplem1  47268  fcores  47544  3f1oss1  47552  uniimaprimaeqfv  47871  elsetpreimafvssdm  47875  gricrel  48424  grlicrel  48511