Theorem cnvimass 6042

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

Syntax hints:   ⊆ wss 3902  ^◡ccnv 5624  dom cdm 5625  ran crn 5626   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  cnvimassrndm  6111  fvimacnvi  6999  elpreima  7005  cnvimainrn  7014  iinpreima  7016  rescnvimafod  7020  fconst4  7162  fsuppeq  8119  fsuppeqg  8120  pw2f1olem  9013  cnvimamptfin  9257  fisuppfi  9278  infxpenlem  9927  enfin2i  10235  fin1a2lem7  10320  smobeth  10501  fpwwe2lem3  10548  fpwwe2lem11  10556  fpwwe2lem12  10557  fpwwe2  10558  canth4  10562  canthwelem  10565  pwfseqlem4  10577  recmulnq  10879  dmrecnq  10883  ltweuz  13888  isercolllem2  15593  isercolllem3  15594  fsumss  15652  ackbijnn  15755  fprodss  15875  1arith  16859  vdwlem1  16913  vdwlem5  16917  vdwlem6  16918  vdwlem8  16920  vdwlem11  16923  ghmpreima  19171  gicer  19210  torsubg  19787  gsumzmhm  19870  gsumzoppg  19877  lmhmpreima  21004  rhmpreimaidl  21236  evpmss  21545  mplcoe5  21999  psr1baslem  22129  ofco2  22399  cnpnei  23212  cnclima  23216  iscncl  23217  cnntri  23219  cnclsi  23220  cncls2  23221  cncls  23222  cnntr  23223  cncnp  23228  cnrest2  23234  cndis  23239  2ndcomap  23406  kgencn  23504  kgencn3  23506  ptbasfi  23529  txcnmpt  23572  txdis1cn  23583  qtopval2  23644  basqtop  23659  qtopcld  23661  qtopcn  23662  qtopeu  23664  qtoprest  23665  hmeoimaf1o  23718  hmphtop  23726  hmpher  23732  ordthmeolem  23749  elfm3  23898  rnelfmlem  23900  rnelfm  23901  fmfnfmlem2  23903  fmfnfmlem4  23905  clssubg  24057  tgphaus  24065  qustgplem  24069  ucnprima  24229  ucncn  24232  xmeter  24381  imasf1oxms  24437  metustss  24499  metustexhalf  24504  metustfbas  24505  cfilucfil  24507  metuel2  24513  restmetu  24518  mbfconstlem  25588  i1fima  25639  i1fima2  25640  i1fd  25642  itg1addlem5  25661  plyeq0lem  26175  dgrcl  26198  dgrub  26199  dgrlb  26201  vieta1lem1  26278  vieta1lem2  26279  pserulm  26391  psercn2  26392  psercn2OLD  26393  psercnlem2  26394  psercnlem1  26395  psercn  26396  pserdvlem1  26397  pserdvlem2  26398  pserdv  26399  pserdv2  26400  abelth  26411  eff1olem  26517  dvlog  26620  logtayl  26629  cxpcn3lem  26717  cxpcn3  26718  resqrtcn  26719  basellem5  27055  elnlfn  32007  nlelshi  32139  xppreima  32726  ofpreima  32746  ofpreima2  32747  fnpreimac  32751  ffsrn  32809  indpreima  32949  indf1ofs  32950  pwrssmgc  33084  elrgspnsubrunlem2  33332  elrspunidl  33511  ply1degltel  33677  ply1degleel  33678  ply1degltlss  33679  esplysply  33731  dimkerim  33786  lvecendof1f1o  33792  locfinreflem  33999  zarcmplem  34040  carsggect  34477  sibfof  34499  sitgclg  34501  eulerpartlemsv2  34517  eulerpartlemsf  34518  eulerpartlemv  34523  eulerpartlemb  34527  eulerpartlemt  34530  eulerpartlemr  34533  eulerpartlemgu  34536  eulerpartlemgs2  34539  eulerpartlemn  34540  cvmliftmolem1  35477  cvmlift2lem9  35507  cvmlift3lem6  35520  cvmlift3lem7  35521  mthmsta  35774  dvtan  37873  itg2addnclem  37874  ftc1anclem6  37901  sstotbnd2  37977  keridl  38235  diaintclN  41386  dibintclN  41495  dihintcl  41672  pw2f1ocnv  43346  dnnumch3lem  43355  dnnumch3  43356  pwfi2f1o  43405  binomcxplemdvbinom  44661  binomcxplemdvsum  44663  binomcxplemnotnn0  44664  wessf1ornlem  45496  sge0f1o  46693  mbfresmf  47050  smfco  47113  smfsuplem1  47122  fcores  47380  3f1oss1  47388  uniimaprimaeqfv  47695  elsetpreimafvssdm  47699  gricrel  48232  grlicrel  48319