Theorem cnvimass 6080

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

Syntax hints:   ⊆ wss 3931  ^◡ccnv 5664  dom cdm 5665  ran crn 5666   “ cima 5668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124  df-opab 5186  df-xp 5671  df-cnv 5673  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678

This theorem is referenced by:  cnvimassrndm  6152  fvimacnvi  7052  elpreima  7058  cnvimainrn  7067  iinpreima  7069  rescnvimafod  7073  fconst4  7216  fsuppeq  8182  fsuppeqg  8183  pw2f1olem  9098  cnvimamptfin  9375  fisuppfi  9393  infxpenlem  10035  enfin2i  10343  fin1a2lem7  10428  smobeth  10608  fpwwe2lem3  10655  fpwwe2lem11  10663  fpwwe2lem12  10664  fpwwe2  10665  canth4  10669  canthwelem  10672  pwfseqlem4  10684  recmulnq  10986  dmrecnq  10990  ltweuz  13984  isercolllem2  15684  isercolllem3  15685  fsumss  15743  ackbijnn  15846  fprodss  15966  1arith  16947  vdwlem1  17001  vdwlem5  17005  vdwlem6  17006  vdwlem8  17008  vdwlem11  17011  ghmpreima  19225  gicer  19264  torsubg  19840  gsumzmhm  19923  gsumzoppg  19930  lmhmpreima  21015  rhmpreimaidl  21249  evpmss  21558  mplcoe5  22012  psr1baslem  22134  ofco2  22405  cnpnei  23218  cnclima  23222  iscncl  23223  cnntri  23225  cnclsi  23226  cncls2  23227  cncls  23228  cnntr  23229  cncnp  23234  cnrest2  23240  cndis  23245  2ndcomap  23412  kgencn  23510  kgencn3  23512  ptbasfi  23535  txcnmpt  23578  txdis1cn  23589  qtopval2  23650  basqtop  23665  qtopcld  23667  qtopcn  23668  qtopeu  23670  qtoprest  23671  hmeoimaf1o  23724  hmphtop  23732  hmpher  23738  ordthmeolem  23755  elfm3  23904  rnelfmlem  23906  rnelfm  23907  fmfnfmlem2  23909  fmfnfmlem4  23911  clssubg  24063  tgphaus  24071  qustgplem  24075  ucnprima  24236  ucncn  24239  xmeter  24388  imasf1oxms  24446  metustss  24508  metustexhalf  24513  metustfbas  24514  cfilucfil  24516  metuel2  24522  restmetu  24527  mbfconstlem  25598  i1fima  25649  i1fima2  25650  i1fd  25652  itg1addlem5  25671  plyeq0lem  26185  dgrcl  26208  dgrub  26209  dgrlb  26211  vieta1lem1  26288  vieta1lem2  26289  pserulm  26401  psercn2  26402  psercn2OLD  26403  psercnlem2  26404  psercnlem1  26405  psercn  26406  pserdvlem1  26407  pserdvlem2  26408  pserdv  26409  pserdv2  26410  abelth  26421  eff1olem  26526  dvlog  26629  logtayl  26638  cxpcn3lem  26726  cxpcn3  26727  resqrtcn  26728  basellem5  27064  elnlfn  31875  nlelshi  32007  xppreima  32590  ofpreima  32610  ofpreima2  32611  fnpreimac  32616  ffsrn  32675  indpreima  32790  indf1ofs  32791  pwrssmgc  32929  elrgspnsubrunlem2  33191  elrspunidl  33391  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  dimkerim  33613  lvecendof1f1o  33619  locfinreflem  33798  zarcmplem  33839  carsggect  34279  sibfof  34301  sitgclg  34303  eulerpartlemsv2  34319  eulerpartlemsf  34320  eulerpartlemv  34325  eulerpartlemb  34329  eulerpartlemt  34332  eulerpartlemr  34335  eulerpartlemgu  34338  eulerpartlemgs2  34341  eulerpartlemn  34342  cvmliftmolem1  35245  cvmlift2lem9  35275  cvmlift3lem6  35288  cvmlift3lem7  35289  mthmsta  35542  dvtan  37636  itg2addnclem  37637  ftc1anclem6  37664  sstotbnd2  37740  keridl  37998  diaintclN  41019  dibintclN  41128  dihintcl  41305  pw2f1ocnv  43012  dnnumch3lem  43021  dnnumch3  43022  pwfi2f1o  43071  binomcxplemdvbinom  44329  binomcxplemdvsum  44331  binomcxplemnotnn0  44332  wessf1ornlem  45147  sge0f1o  46354  mbfresmf  46711  smfco  46774  smfsuplem1  46783  fcores  47037  3f1oss1  47045  uniimaprimaeqfv  47327  elsetpreimafvssdm  47331  gricrel  47846  grlicrel  47924