Theorem cnvimass 6079

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

Syntax hints:   ⊆ wss 3947  ^◡ccnv 5674  dom cdm 5675  ran crn 5676   “ cima 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688

This theorem is referenced by:  cnvimassrndm  6150  fvimacnvi  7052  elpreima  7058  cnvimainrn  7067  iinpreima  7069  rescnvimafod  7074  fconst4  7217  fsuppeq  8162  fsuppeqg  8163  pw2f1olem  9078  cnvimamptfin  9355  fisuppfi  9372  infxpenlem  10010  enfin2i  10318  fin1a2lem7  10403  smobeth  10583  fpwwe2lem3  10630  fpwwe2lem11  10638  fpwwe2lem12  10639  fpwwe2  10640  canth4  10644  canthwelem  10647  pwfseqlem4  10659  recmulnq  10961  dmrecnq  10965  ltweuz  13930  isercolllem2  15616  isercolllem3  15617  fsumss  15675  ackbijnn  15778  fprodss  15896  1arith  16864  vdwlem1  16918  vdwlem5  16922  vdwlem6  16923  vdwlem8  16925  vdwlem11  16928  ghmpreima  19152  gicer  19191  torsubg  19763  gsumzmhm  19846  gsumzoppg  19853  lmhmpreima  20803  evpmss  21358  mplcoe5  21814  psr1baslem  21928  ofco2  22173  cnpnei  22988  cnclima  22992  iscncl  22993  cnntri  22995  cnclsi  22996  cncls2  22997  cncls  22998  cnntr  22999  cncnp  23004  cnrest2  23010  cndis  23015  2ndcomap  23182  kgencn  23280  kgencn3  23282  ptbasfi  23305  txcnmpt  23348  txdis1cn  23359  qtopval2  23420  basqtop  23435  qtopcld  23437  qtopcn  23438  qtopeu  23440  qtoprest  23441  hmeoimaf1o  23494  hmphtop  23502  hmpher  23508  ordthmeolem  23525  elfm3  23674  rnelfmlem  23676  rnelfm  23677  fmfnfmlem2  23679  fmfnfmlem4  23681  clssubg  23833  tgphaus  23841  qustgplem  23845  ucnprima  24007  ucncn  24010  xmeter  24159  imasf1oxms  24218  metustss  24280  metustexhalf  24285  metustfbas  24286  cfilucfil  24288  metuel2  24294  restmetu  24299  mbfconstlem  25376  i1fima  25427  i1fima2  25428  i1fd  25430  itg1addlem5  25450  plyeq0lem  25959  dgrcl  25982  dgrub  25983  dgrlb  25985  vieta1lem1  26059  vieta1lem2  26060  pserulm  26170  psercn2  26171  psercnlem2  26172  psercnlem1  26173  psercn  26174  pserdvlem1  26175  pserdvlem2  26176  pserdv  26177  pserdv2  26178  abelth  26189  eff1olem  26293  dvlog  26395  logtayl  26404  cxpcn3lem  26491  cxpcn3  26492  resqrtcn  26493  basellem5  26825  elnlfn  31448  nlelshi  31580  xppreima  32138  ofpreima  32157  ofpreima2  32158  fnpreimac  32163  ffsrn  32221  pwrssmgc  32437  rhmpreimaidl  32811  elrspunidl  32820  ply1degltel  32940  ply1degleel  32941  ply1degltlss  32942  dimkerim  33000  locfinreflem  33118  zarcmplem  33159  indpreima  33321  indf1ofs  33322  carsggect  33615  sibfof  33637  sitgclg  33639  eulerpartlemsv2  33655  eulerpartlemsf  33656  eulerpartlemv  33661  eulerpartlemb  33665  eulerpartlemt  33668  eulerpartlemr  33671  eulerpartlemgu  33674  eulerpartlemgs2  33677  eulerpartlemn  33678  cvmliftmolem1  34570  cvmlift2lem9  34600  cvmlift3lem6  34613  cvmlift3lem7  34614  mthmsta  34867  gg-psercn2  35464  dvtan  36841  itg2addnclem  36842  ftc1anclem6  36869  sstotbnd2  36945  keridl  37203  diaintclN  40232  dibintclN  40341  dihintcl  40518  pw2f1ocnv  42078  dnnumch3lem  42090  dnnumch3  42091  pwfi2f1o  42140  binomcxplemdvbinom  43414  binomcxplemdvsum  43416  binomcxplemnotnn0  43417  wessf1ornlem  44182  sge0f1o  45396  mbfresmf  45753  smfco  45816  smfsuplem1  45825  fcores  46075  uniimaprimaeqfv  46348  elsetpreimafvssdm  46352