Theorem cnvimass 6073

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

Syntax hints:   ⊆ wss 3906  ^◡ccnv 5648  dom cdm 5649  ran crn 5650   “ cima 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103  df-opab 5165  df-xp 5655  df-cnv 5657  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662

This theorem is referenced by:  cnvimassrndm  6139  fvimacnvi  7035  elpreima  7041  cnvimainrn  7050  iinpreima  7052  rescnvimafod  7056  fconst4  7200  fsuppeq  8157  fsuppeqg  8158  pw2f1olem  9055  cnvimamptfin  9298  fisuppfi  9319  infxpenlem  9971  enfin2i  10280  fin1a2lem7  10365  smobeth  10546  fpwwe2lem3  10593  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  canth4  10607  canthwelem  10610  pwfseqlem4  10622  recmulnq  10924  dmrecnq  10928  ltweuz  13976  isercolllem2  15695  isercolllem3  15696  fsumss  15754  ackbijnn  15860  fprodss  15980  1arith  16965  vdwlem1  17019  vdwlem5  17023  vdwlem6  17024  vdwlem8  17026  vdwlem11  17029  ghmpreima  19280  gicer  19319  torsubg  19896  gsumzmhm  19979  gsumzoppg  19986  lmhmpreima  21117  rhmpreimaidl  21349  evpmss  21640  mplcoe5  22095  psr1baslem  22249  ofco2  22513  cnpnei  23326  cnclima  23330  iscncl  23331  cnntri  23333  cnclsi  23334  cncls2  23335  cncls  23336  cnntr  23337  cncnp  23342  cnrest2  23348  cndis  23353  2ndcomap  23520  kgencn  23618  kgencn3  23620  ptbasfi  23643  txcnmpt  23686  txdis1cn  23697  qtopval2  23758  basqtop  23773  qtopcld  23775  qtopcn  23776  qtopeu  23778  qtoprest  23779  hmeoimaf1o  23832  hmphtop  23840  hmpher  23846  ordthmeolem  23863  elfm3  24012  rnelfmlem  24014  rnelfm  24015  fmfnfmlem2  24017  fmfnfmlem4  24019  clssubg  24171  tgphaus  24179  qustgplem  24183  ucnprima  24343  ucncn  24346  xmeter  24495  imasf1oxms  24551  metustss  24613  metustexhalf  24618  metustfbas  24619  cfilucfil  24621  metuel2  24627  restmetu  24632  mbfconstlem  25691  i1fima  25742  i1fima2  25743  i1fd  25745  itg1addlem5  25764  plyeq0lem  26272  dgrcl  26295  dgrub  26296  dgrlb  26298  vieta1lem1  26376  vieta1lem2  26377  pserulm  26487  psercn2  26488  psercnlem2  26489  psercnlem1  26490  psercn  26491  pserdvlem1  26492  pserdvlem2  26493  pserdv  26494  pserdv2  26495  abelth  26506  eff1olem  26615  dvlog  26718  logtayl  26727  cxpcn3lem  26814  cxpcn3  26815  resqrtcn  26816  basellem5  27151  elnlfn  32133  nlelshi  32265  xppreima  32849  ofpreima  32869  ofpreima2  32870  fnpreimac  32874  ffsrn  32932  indpreima  33045  indf1ofs  33046  pwrssmgc  33180  elrgspnsubrunlem2  33431  elrspunidl  33616  ply1degltel  33792  ply1degleel  33793  ply1degltlss  33794  esplysply  33870  dimkerim  33926  lvecendof1f1o  33932  locfinreflem  34139  zarcmplem  34180  carsggect  34617  sibfof  34639  sitgclg  34641  eulerpartlemsv2  34657  eulerpartlemsf  34658  eulerpartlemv  34663  eulerpartlemb  34667  eulerpartlemt  34670  eulerpartlemr  34673  eulerpartlemgu  34676  eulerpartlemgs2  34679  eulerpartlemn  34680  onvfowev  35463  cvmliftmolem1  35636  cvmlift2lem9  35666  cvmlift3lem6  35679  cvmlift3lem7  35680  mthmsta  35933  dvtan  38174  itg2addnclem  38175  ftc1anclem6  38202  sstotbnd2  38278  keridl  38536  diaintclN  41687  dibintclN  41796  dihintcl  41973  pw2f1ocnv  43619  dnnumch3lem  43628  dnnumch3  43629  pwfi2f1o  43678  binomcxplemdvbinom  44934  binomcxplemdvsum  44936  binomcxplemnotnn0  44937  wessf1ornlem  45768  sge0f1o  46961  mbfresmf  47318  smfco  47381  smfsuplem1  47390  fcores  47666  3f1oss1  47674  uniimaprimaeqfv  47993  elsetpreimafvssdm  47997  gricrel  48546  grlicrel  48633