Theorem cnvimass 6111

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

Syntax hints:   ⊆ wss 3976  ^◡ccnv 5699  dom cdm 5700  ran crn 5701   “ cima 5703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713

This theorem is referenced by:  cnvimassrndm  6183  fvimacnvi  7085  elpreima  7091  cnvimainrn  7100  iinpreima  7102  rescnvimafod  7107  fconst4  7251  fsuppeq  8216  fsuppeqg  8217  pw2f1olem  9142  cnvimamptfin  9423  fisuppfi  9441  infxpenlem  10082  enfin2i  10390  fin1a2lem7  10475  smobeth  10655  fpwwe2lem3  10702  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  canth4  10716  canthwelem  10719  pwfseqlem4  10731  recmulnq  11033  dmrecnq  11037  ltweuz  14012  isercolllem2  15714  isercolllem3  15715  fsumss  15773  ackbijnn  15876  fprodss  15996  1arith  16974  vdwlem1  17028  vdwlem5  17032  vdwlem6  17033  vdwlem8  17035  vdwlem11  17038  ghmpreima  19278  gicer  19317  torsubg  19896  gsumzmhm  19979  gsumzoppg  19986  lmhmpreima  21070  rhmpreimaidl  21310  evpmss  21627  mplcoe5  22081  psr1baslem  22207  ofco2  22478  cnpnei  23293  cnclima  23297  iscncl  23298  cnntri  23300  cnclsi  23301  cncls2  23302  cncls  23303  cnntr  23304  cncnp  23309  cnrest2  23315  cndis  23320  2ndcomap  23487  kgencn  23585  kgencn3  23587  ptbasfi  23610  txcnmpt  23653  txdis1cn  23664  qtopval2  23725  basqtop  23740  qtopcld  23742  qtopcn  23743  qtopeu  23745  qtoprest  23746  hmeoimaf1o  23799  hmphtop  23807  hmpher  23813  ordthmeolem  23830  elfm3  23979  rnelfmlem  23981  rnelfm  23982  fmfnfmlem2  23984  fmfnfmlem4  23986  clssubg  24138  tgphaus  24146  qustgplem  24150  ucnprima  24312  ucncn  24315  xmeter  24464  imasf1oxms  24523  metustss  24585  metustexhalf  24590  metustfbas  24591  cfilucfil  24593  metuel2  24599  restmetu  24604  mbfconstlem  25681  i1fima  25732  i1fima2  25733  i1fd  25735  itg1addlem5  25755  plyeq0lem  26269  dgrcl  26292  dgrub  26293  dgrlb  26295  vieta1lem1  26370  vieta1lem2  26371  pserulm  26483  psercn2  26484  psercn2OLD  26485  psercnlem2  26486  psercnlem1  26487  psercn  26488  pserdvlem1  26489  pserdvlem2  26490  pserdv  26491  pserdv2  26492  abelth  26503  eff1olem  26608  dvlog  26711  logtayl  26720  cxpcn3lem  26808  cxpcn3  26809  resqrtcn  26810  basellem5  27146  elnlfn  31960  nlelshi  32092  xppreima  32664  ofpreima  32683  ofpreima2  32684  fnpreimac  32689  ffsrn  32743  pwrssmgc  32973  elrspunidl  33421  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  dimkerim  33640  lvecendof1f1o  33646  locfinreflem  33786  zarcmplem  33827  indpreima  33989  indf1ofs  33990  carsggect  34283  sibfof  34305  sitgclg  34307  eulerpartlemsv2  34323  eulerpartlemsf  34324  eulerpartlemv  34329  eulerpartlemb  34333  eulerpartlemt  34336  eulerpartlemr  34339  eulerpartlemgu  34342  eulerpartlemgs2  34345  eulerpartlemn  34346  cvmliftmolem1  35249  cvmlift2lem9  35279  cvmlift3lem6  35292  cvmlift3lem7  35293  mthmsta  35546  dvtan  37630  itg2addnclem  37631  ftc1anclem6  37658  sstotbnd2  37734  keridl  37992  diaintclN  41015  dibintclN  41124  dihintcl  41301  pw2f1ocnv  42994  dnnumch3lem  43003  dnnumch3  43004  pwfi2f1o  43053  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  wessf1ornlem  45092  sge0f1o  46303  mbfresmf  46660  smfco  46723  smfsuplem1  46732  fcores  46982  3f1oss1  46990  uniimaprimaeqfv  47256  elsetpreimafvssdm  47260  gricrel  47772  grlicrel  47823