Theorem cnvimass 6047

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

Syntax hints:   ⊆ wss 3889  ^◡ccnv 5630  dom cdm 5631  ran crn 5632   “ cima 5634

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  cnvimassrndm  6116  fvimacnvi  7004  elpreima  7010  cnvimainrn  7019  iinpreima  7021  rescnvimafod  7025  fconst4  7169  fsuppeq  8125  fsuppeqg  8126  pw2f1olem  9019  cnvimamptfin  9263  fisuppfi  9284  infxpenlem  9935  enfin2i  10243  fin1a2lem7  10328  smobeth  10509  fpwwe2lem3  10556  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  canth4  10570  canthwelem  10573  pwfseqlem4  10585  recmulnq  10887  dmrecnq  10891  ltweuz  13923  isercolllem2  15628  isercolllem3  15629  fsumss  15687  ackbijnn  15793  fprodss  15913  1arith  16898  vdwlem1  16952  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  vdwlem11  16962  ghmpreima  19213  gicer  19252  torsubg  19829  gsumzmhm  19912  gsumzoppg  19919  lmhmpreima  21043  rhmpreimaidl  21275  evpmss  21566  mplcoe5  22018  psr1baslem  22148  ofco2  22416  cnpnei  23229  cnclima  23233  iscncl  23234  cnntri  23236  cnclsi  23237  cncls2  23238  cncls  23239  cnntr  23240  cncnp  23245  cnrest2  23251  cndis  23256  2ndcomap  23423  kgencn  23521  kgencn3  23523  ptbasfi  23546  txcnmpt  23589  txdis1cn  23600  qtopval2  23661  basqtop  23676  qtopcld  23678  qtopcn  23679  qtopeu  23681  qtoprest  23682  hmeoimaf1o  23735  hmphtop  23743  hmpher  23749  ordthmeolem  23766  elfm3  23915  rnelfmlem  23917  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem4  23922  clssubg  24074  tgphaus  24082  qustgplem  24086  ucnprima  24246  ucncn  24249  xmeter  24398  imasf1oxms  24454  metustss  24516  metustexhalf  24521  metustfbas  24522  cfilucfil  24524  metuel2  24530  restmetu  24535  mbfconstlem  25594  i1fima  25645  i1fima2  25646  i1fd  25648  itg1addlem5  25667  plyeq0lem  26175  dgrcl  26198  dgrub  26199  dgrlb  26201  vieta1lem1  26276  vieta1lem2  26277  pserulm  26387  psercn2  26388  psercnlem2  26389  psercnlem1  26390  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  pserdv  26394  pserdv2  26395  abelth  26406  eff1olem  26512  dvlog  26615  logtayl  26624  cxpcn3lem  26711  cxpcn3  26712  resqrtcn  26713  basellem5  27048  elnlfn  31999  nlelshi  32131  xppreima  32718  ofpreima  32738  ofpreima2  32739  fnpreimac  32743  ffsrn  32801  indpreima  32925  indf1ofs  32926  pwrssmgc  33060  elrgspnsubrunlem2  33309  elrspunidl  33488  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  esplysply  33715  dimkerim  33771  lvecendof1f1o  33777  locfinreflem  33984  zarcmplem  34025  carsggect  34462  sibfof  34484  sitgclg  34486  eulerpartlemsv2  34502  eulerpartlemsf  34503  eulerpartlemv  34508  eulerpartlemb  34512  eulerpartlemt  34515  eulerpartlemr  34518  eulerpartlemgu  34521  eulerpartlemgs2  34524  eulerpartlemn  34525  cvmliftmolem1  35463  cvmlift2lem9  35493  cvmlift3lem6  35506  cvmlift3lem7  35507  mthmsta  35760  dvtan  37991  itg2addnclem  37992  ftc1anclem6  38019  sstotbnd2  38095  keridl  38353  diaintclN  41504  dibintclN  41613  dihintcl  41790  pw2f1ocnv  43465  dnnumch3lem  43474  dnnumch3  43475  pwfi2f1o  43524  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  wessf1ornlem  45615  sge0f1o  46810  mbfresmf  47167  smfco  47230  smfsuplem1  47239  fcores  47515  3f1oss1  47523  uniimaprimaeqfv  47842  elsetpreimafvssdm  47846  gricrel  48395  grlicrel  48482