Theorem cnvimass 6051

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

Syntax hints:   ⊆ wss 3903  ^◡ccnv 5633  dom cdm 5634  ran crn 5635   “ cima 5637

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 5245  ax-pr 5381

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 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5640  df-cnv 5642  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647

This theorem is referenced by:  cnvimassrndm  6120  fvimacnvi  7008  elpreima  7014  cnvimainrn  7023  iinpreima  7025  rescnvimafod  7029  fconst4  7172  fsuppeq  8129  fsuppeqg  8130  pw2f1olem  9023  cnvimamptfin  9267  fisuppfi  9288  infxpenlem  9937  enfin2i  10245  fin1a2lem7  10330  smobeth  10511  fpwwe2lem3  10558  fpwwe2lem11  10566  fpwwe2lem12  10567  fpwwe2  10568  canth4  10572  canthwelem  10575  pwfseqlem4  10587  recmulnq  10889  dmrecnq  10893  ltweuz  13898  isercolllem2  15603  isercolllem3  15604  fsumss  15662  ackbijnn  15765  fprodss  15885  1arith  16869  vdwlem1  16923  vdwlem5  16927  vdwlem6  16928  vdwlem8  16930  vdwlem11  16933  ghmpreima  19184  gicer  19223  torsubg  19800  gsumzmhm  19883  gsumzoppg  19890  lmhmpreima  21017  rhmpreimaidl  21249  evpmss  21558  mplcoe5  22012  psr1baslem  22142  ofco2  22412  cnpnei  23225  cnclima  23229  iscncl  23230  cnntri  23232  cnclsi  23233  cncls2  23234  cncls  23235  cnntr  23236  cncnp  23241  cnrest2  23247  cndis  23252  2ndcomap  23419  kgencn  23517  kgencn3  23519  ptbasfi  23542  txcnmpt  23585  txdis1cn  23596  qtopval2  23657  basqtop  23672  qtopcld  23674  qtopcn  23675  qtopeu  23677  qtoprest  23678  hmeoimaf1o  23731  hmphtop  23739  hmpher  23745  ordthmeolem  23762  elfm3  23911  rnelfmlem  23913  rnelfm  23914  fmfnfmlem2  23916  fmfnfmlem4  23918  clssubg  24070  tgphaus  24078  qustgplem  24082  ucnprima  24242  ucncn  24245  xmeter  24394  imasf1oxms  24450  metustss  24512  metustexhalf  24517  metustfbas  24518  cfilucfil  24520  metuel2  24526  restmetu  24531  mbfconstlem  25601  i1fima  25652  i1fima2  25653  i1fd  25655  itg1addlem5  25674  plyeq0lem  26188  dgrcl  26211  dgrub  26212  dgrlb  26214  vieta1lem1  26291  vieta1lem2  26292  pserulm  26404  psercn2  26405  psercn2OLD  26406  psercnlem2  26407  psercnlem1  26408  psercn  26409  pserdvlem1  26410  pserdvlem2  26411  pserdv  26412  pserdv2  26413  abelth  26424  eff1olem  26530  dvlog  26633  logtayl  26642  cxpcn3lem  26730  cxpcn3  26731  resqrtcn  26732  basellem5  27068  elnlfn  32022  nlelshi  32154  xppreima  32741  ofpreima  32761  ofpreima2  32762  fnpreimac  32766  ffsrn  32824  indpreima  32964  indf1ofs  32965  pwrssmgc  33099  elrgspnsubrunlem2  33348  elrspunidl  33527  ply1degltel  33693  ply1degleel  33694  ply1degltlss  33695  esplysply  33754  dimkerim  33811  lvecendof1f1o  33817  locfinreflem  34024  zarcmplem  34065  carsggect  34502  sibfof  34524  sitgclg  34526  eulerpartlemsv2  34542  eulerpartlemsf  34543  eulerpartlemv  34548  eulerpartlemb  34552  eulerpartlemt  34555  eulerpartlemr  34558  eulerpartlemgu  34561  eulerpartlemgs2  34564  eulerpartlemn  34565  cvmliftmolem1  35503  cvmlift2lem9  35533  cvmlift3lem6  35546  cvmlift3lem7  35547  mthmsta  35800  dvtan  37950  itg2addnclem  37951  ftc1anclem6  37978  sstotbnd2  38054  keridl  38312  diaintclN  41463  dibintclN  41572  dihintcl  41749  pw2f1ocnv  43423  dnnumch3lem  43432  dnnumch3  43433  pwfi2f1o  43482  binomcxplemdvbinom  44738  binomcxplemdvsum  44740  binomcxplemnotnn0  44741  wessf1ornlem  45573  sge0f1o  46769  mbfresmf  47126  smfco  47189  smfsuplem1  47198  fcores  47456  3f1oss1  47464  uniimaprimaeqfv  47771  elsetpreimafvssdm  47775  gricrel  48308  grlicrel  48395