Theorem cnvimass 6084

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

This proof depends on syntax axioms:   ⊆ wss 3905  ^◡ccnv 5660  dom cdm 5661  ran crn 5662   “ cima 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674

This theorem is used by:  cnvimassrndm  6149  fvimacnvi  7047  elpreima  7053  cnvimainrn  7062  iinpreima  7064  rescnvimafod  7068  fconst4  7212  fsuppeq  8167  fsuppeqg  8168  pw2f1olem  9065  cnvimamptfin  9306  fisuppfi  9327  infxpenlem  10002  enfin2i  10309  fin1a2lem7  10394  smobeth  10575  fpwwe2lem3  10622  fpwwe2lem11  10630  fpwwe2lem12  10631  fpwwe2  10632  canth4  10636  canthwelem  10639  pwfseqlem4  10651  recmulnq  10953  dmrecnq  10957  ltweuz  14002  isercolllem2  15722  isercolllem3  15723  fsumss  15781  ackbijnn  15887  fprodss  16007  1arith  16991  vdwlem1  17045  vdwlem5  17049  vdwlem6  17050  vdwlem8  17052  vdwlem11  17055  ghmpreima  19312  gicer  19351  torsubg  19928  gsumzmhm  20011  gsumzoppg  20018  ricrel  20601  lmhmpreima  21178  rhmpreimaidl  21425  evpmss  21745  mplcoe5  22200  psr1baslem  22354  ofco2  22617  cnpnei  23430  cnclima  23434  iscncl  23435  cnntri  23437  cnclsi  23438  cncls2  23439  cncls  23440  cnntr  23441  cncnp  23446  cnrest2  23452  cndis  23457  2ndcomap  23624  kgencn  23722  kgencn3  23724  ptbasfi  23747  txcnmpt  23790  txdis1cn  23801  qtopval2  23862  basqtop  23877  qtopcld  23879  qtopcn  23880  qtopeu  23882  qtoprest  23883  hmeoimaf1o  23936  hmphtop  23944  hmpher  23950  ordthmeolem  23967  elfm3  24116  rnelfmlem  24118  rnelfm  24119  fmfnfmlem2  24121  fmfnfmlem4  24123  clssubg  24275  tgphaus  24283  qustgplem  24287  ucnprima  24447  ucncn  24450  xmeter  24599  imasf1oxms  24655  metustss  24717  metustexhalf  24722  metustfbas  24723  cfilucfil  24725  metuel2  24731  restmetu  24736  mbfconstlem  25795  i1fima  25846  i1fima2  25847  i1fd  25849  itg1addlem5  25868  plyeq0lem  26376  dgrcl  26399  dgrub  26400  dgrlb  26402  vieta1lem1  26480  vieta1lem2  26481  pserulm  26594  psercn2  26595  psercnlem2  26596  psercnlem1  26597  psercn  26598  pserdvlem1  26599  pserdvlem2  26600  pserdv  26601  pserdv2  26602  abelth  26613  eff1olem  26722  dvlog  26825  logtayl  26834  cxpcn3lem  26921  cxpcn3  26922  resqrtcn  26923  basellem5  27258  elnlfn  32289  nlelshi  32421  xppreima  32999  ofpreima  33019  ofpreima2  33020  fnpreimac  33024  ffsrn  33082  indpreima  33194  indf1ofs  33195  pwrssmgc  33329  elrgspnsubrunlem2  33577  elrspunidl  33745  ply1degltel  33893  ply1degleel  33894  ply1degltlss  33895  esplysply  33970  dimkerim  34026  lvecendof1f1o  34032  locfinreflem  34239  zarcmplem  34280  carsggect  34717  sibfof  34739  sitgclg  34741  eulerpartlemsv2  34757  eulerpartlemsf  34758  eulerpartlemv  34763  eulerpartlemb  34767  eulerpartlemt  34770  eulerpartlemr  34773  eulerpartlemgu  34776  eulerpartlemgs2  34779  eulerpartlemn  34780  onvfowev  35608  cvmliftmolem1  35781  cvmlift2lem9  35811  cvmlift3lem6  35824  cvmlift3lem7  35825  mthmsta  36078  dvtan  38349  itg2addnclem  38350  ftc1anclem6  38377  sstotbnd2  38453  keridl  38711  diaintclN  41860  dibintclN  41969  dihintcl  42146  pw2f1ocnv  43792  dnnumch3lem  43801  dnnumch3  43802  pwfi2f1o  43851  binomcxplemdvbinom  45091  binomcxplemdvsum  45093  binomcxplemnotnn0  45094  wessf1ornlem  45931  sge0f1o  47124  mbfresmf  47481  smfco  47544  smfsuplem1  47553  fcores  47832  3f1oss1  47840  uniimaprimaeqfv  48159  elsetpreimafvssdm  48163  gricrel  48712  grlicrel  48799