Theorem cnvimass 6085

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

Syntax hints:   ⊆ wss 3913  ^◡ccnv 5661  dom cdm 5662  ran crn 5663   “ cima 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675

This theorem is referenced by:  cnvimassrndm  6150  fvimacnvi  7048  elpreima  7054  cnvimainrn  7063  iinpreima  7065  rescnvimafod  7069  fconst4  7213  fsuppeq  8171  fsuppeqg  8172  pw2f1olem  9069  cnvimamptfin  9310  fisuppfi  9331  infxpenlem  9997  enfin2i  10305  fin1a2lem7  10390  smobeth  10571  fpwwe2lem3  10618  fpwwe2lem11  10626  fpwwe2lem12  10627  fpwwe2  10628  canth4  10632  canthwelem  10635  pwfseqlem4  10647  recmulnq  10949  dmrecnq  10953  ltweuz  13997  isercolllem2  15717  isercolllem3  15718  fsumss  15776  ackbijnn  15882  fprodss  16002  1arith  16987  vdwlem1  17041  vdwlem5  17045  vdwlem6  17046  vdwlem8  17048  vdwlem11  17051  ghmpreima  19308  gicer  19347  torsubg  19924  gsumzmhm  20007  gsumzoppg  20014  lmhmpreima  21147  rhmpreimaidl  21387  evpmss  21705  mplcoe5  22160  psr1baslem  22314  ofco2  22577  cnpnei  23390  cnclima  23394  iscncl  23395  cnntri  23397  cnclsi  23398  cncls2  23399  cncls  23400  cnntr  23401  cncnp  23406  cnrest2  23412  cndis  23417  2ndcomap  23584  kgencn  23682  kgencn3  23684  ptbasfi  23707  txcnmpt  23750  txdis1cn  23761  qtopval2  23822  basqtop  23837  qtopcld  23839  qtopcn  23840  qtopeu  23842  qtoprest  23843  hmeoimaf1o  23896  hmphtop  23904  hmpher  23910  ordthmeolem  23927  elfm3  24076  rnelfmlem  24078  rnelfm  24079  fmfnfmlem2  24081  fmfnfmlem4  24083  clssubg  24235  tgphaus  24243  qustgplem  24247  ucnprima  24407  ucncn  24410  xmeter  24559  imasf1oxms  24615  metustss  24677  metustexhalf  24682  metustfbas  24683  cfilucfil  24685  metuel2  24691  restmetu  24696  mbfconstlem  25755  i1fima  25806  i1fima2  25807  i1fd  25809  itg1addlem5  25828  plyeq0lem  26336  dgrcl  26359  dgrub  26360  dgrlb  26362  vieta1lem1  26440  vieta1lem2  26441  pserulm  26551  psercn2  26552  psercnlem2  26553  psercnlem1  26554  psercn  26555  pserdvlem1  26556  pserdvlem2  26557  pserdv  26558  pserdv2  26559  abelth  26570  eff1olem  26679  dvlog  26782  logtayl  26791  cxpcn3lem  26878  cxpcn3  26879  resqrtcn  26880  basellem5  27215  elnlfn  32221  nlelshi  32353  xppreima  32931  ofpreima  32951  ofpreima2  32952  fnpreimac  32956  ffsrn  33014  indpreima  33126  indf1ofs  33127  pwrssmgc  33261  elrgspnsubrunlem2  33509  elrspunidl  33680  ply1degltel  33829  ply1degleel  33830  ply1degltlss  33831  esplysply  33906  dimkerim  33962  lvecendof1f1o  33968  locfinreflem  34175  zarcmplem  34216  carsggect  34653  sibfof  34675  sitgclg  34677  eulerpartlemsv2  34693  eulerpartlemsf  34694  eulerpartlemv  34699  eulerpartlemb  34703  eulerpartlemt  34706  eulerpartlemr  34709  eulerpartlemgu  34712  eulerpartlemgs2  34715  eulerpartlemn  34716  onvfowev  35533  cvmliftmolem1  35706  cvmlift2lem9  35736  cvmlift3lem6  35749  cvmlift3lem7  35750  mthmsta  36003  dvtan  38243  itg2addnclem  38244  ftc1anclem6  38271  sstotbnd2  38347  keridl  38605  diaintclN  41756  dibintclN  41865  dihintcl  42042  pw2f1ocnv  43690  dnnumch3lem  43699  dnnumch3  43700  pwfi2f1o  43749  binomcxplemdvbinom  44989  binomcxplemdvsum  44991  binomcxplemnotnn0  44992  wessf1ornlem  45829  sge0f1o  47022  mbfresmf  47379  smfco  47442  smfsuplem1  47451  fcores  47727  3f1oss1  47735  uniimaprimaeqfv  48054  elsetpreimafvssdm  48058  gricrel  48607  grlicrel  48694