Theorem cnvimass 6081

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

Syntax hints:   ⊆ wss 3949  ^◡ccnv 5676  dom cdm 5677  ran crn 5678   “ cima 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690

This theorem is referenced by:  cnvimassrndm  6152  fvimacnvi  7054  elpreima  7060  cnvimainrn  7069  iinpreima  7071  rescnvimafod  7076  fconst4  7216  fsuppeq  8160  fsuppeqg  8161  pw2f1olem  9076  cnvimamptfin  9353  fisuppfi  9370  infxpenlem  10008  enfin2i  10316  fin1a2lem7  10401  smobeth  10581  fpwwe2lem3  10628  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  canth4  10642  canthwelem  10645  pwfseqlem4  10657  recmulnq  10959  dmrecnq  10963  ltweuz  13926  isercolllem2  15612  isercolllem3  15613  fsumss  15671  ackbijnn  15774  fprodss  15892  1arith  16860  vdwlem1  16914  vdwlem5  16918  vdwlem6  16919  vdwlem8  16921  vdwlem11  16924  ghmpreima  19114  gicer  19150  torsubg  19722  gsumzmhm  19805  gsumzoppg  19812  lmhmpreima  20659  evpmss  21139  mplcoe5  21595  psr1baslem  21709  ofco2  21953  cnpnei  22768  cnclima  22772  iscncl  22773  cnntri  22775  cnclsi  22776  cncls2  22777  cncls  22778  cnntr  22779  cncnp  22784  cnrest2  22790  cndis  22795  2ndcomap  22962  kgencn  23060  kgencn3  23062  ptbasfi  23085  txcnmpt  23128  txdis1cn  23139  qtopval2  23200  basqtop  23215  qtopcld  23217  qtopcn  23218  qtopeu  23220  qtoprest  23221  hmeoimaf1o  23274  hmphtop  23282  hmpher  23288  ordthmeolem  23305  elfm3  23454  rnelfmlem  23456  rnelfm  23457  fmfnfmlem2  23459  fmfnfmlem4  23461  clssubg  23613  tgphaus  23621  qustgplem  23625  ucnprima  23787  ucncn  23790  xmeter  23939  imasf1oxms  23998  metustss  24060  metustexhalf  24065  metustfbas  24066  cfilucfil  24068  metuel2  24074  restmetu  24079  mbfconstlem  25144  i1fima  25195  i1fima2  25196  i1fd  25198  itg1addlem5  25218  plyeq0lem  25724  dgrcl  25747  dgrub  25748  dgrlb  25750  vieta1lem1  25823  vieta1lem2  25824  pserulm  25934  psercn2  25935  psercnlem2  25936  psercnlem1  25937  psercn  25938  pserdvlem1  25939  pserdvlem2  25940  pserdv  25941  pserdv2  25942  abelth  25953  eff1olem  26057  dvlog  26159  logtayl  26168  cxpcn3lem  26255  cxpcn3  26256  resqrtcn  26257  basellem5  26589  elnlfn  31181  nlelshi  31313  xppreima  31871  ofpreima  31890  ofpreima2  31891  fnpreimac  31896  ffsrn  31954  pwrssmgc  32170  rhmpreimaidl  32537  elrspunidl  32546  ply1degltel  32666  ply1degltlss  32667  dimkerim  32712  locfinreflem  32820  zarcmplem  32861  indpreima  33023  indf1ofs  33024  carsggect  33317  sibfof  33339  sitgclg  33341  eulerpartlemsv2  33357  eulerpartlemsf  33358  eulerpartlemv  33363  eulerpartlemb  33367  eulerpartlemt  33370  eulerpartlemr  33373  eulerpartlemgu  33376  eulerpartlemgs2  33379  eulerpartlemn  33380  cvmliftmolem1  34272  cvmlift2lem9  34302  cvmlift3lem6  34315  cvmlift3lem7  34316  mthmsta  34569  gg-psercn2  35178  dvtan  36538  itg2addnclem  36539  ftc1anclem6  36566  sstotbnd2  36642  keridl  36900  diaintclN  39929  dibintclN  40038  dihintcl  40215  pw2f1ocnv  41776  dnnumch3lem  41788  dnnumch3  41789  pwfi2f1o  41838  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  wessf1ornlem  43882  sge0f1o  45098  mbfresmf  45455  smfco  45518  smfsuplem1  45527  fcores  45777  uniimaprimaeqfv  46050  elsetpreimafvssdm  46054