Theorem cnvimass 6079

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

This proof depends on syntax axioms:   ⊆ wss 3899  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   “ cima 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  cnvimassrndm  6144  fvimacnvi  7046  elpreima  7052  cnvimainrn  7061  iinpreima  7064  rescnvimafod  7068  fconst4  7215  fsuppeq  8175  fsuppeqg  8176  pw2f1olem  9083  cnvimamptfin  9324  fisuppfi  9345  infxpenlem  10038  enfin2i  10345  fin1a2lem7  10430  smobeth  10617  fpwwe2lem3  10664  fpwwe2lem11  10672  fpwwe2lem12  10673  fpwwe2  10674  canth4  10678  canthwelem  10681  pwfseqlem4  10693  recmulnq  10995  dmrecnq  10999  ltweuz  14047  isercolllem2  15775  isercolllem3  15776  fsumss  15833  ackbijnn  15939  fprodss  16057  1arith  17041  vdwlem1  17095  vdwlem5  17099  vdwlem6  17100  vdwlem8  17102  vdwlem11  17105  ghmpreima  19388  gicer  19427  torsubg  20004  gsumzmhm  20087  gsumzoppg  20094  ricrel  20680  lmhmpreima  21259  rhmpreimaidl  21507  evpmss  21828  mplcoe5  22285  psr1baslem  22439  ofco2  22702  cnpnei  23518  cnclima  23522  iscncl  23523  cnntri  23525  cnclsi  23526  cncls2  23527  cncls  23528  cnntr  23529  cncnp  23534  cnrest2  23540  cndis  23545  2ndcomap  23713  kgencn  23811  kgencn3  23813  ptbasfi  23836  txcnmpt  23879  txdis1cn  23890  qtopval2  23951  basqtop  23966  qtopcld  23968  qtopcn  23969  qtopeu  23971  qtoprest  23972  hmeoimaf1o  24025  hmphtop  24033  hmpher  24039  ordthmeolem  24056  elfm3  24205  rnelfmlem  24207  rnelfm  24208  fmfnfmlem2  24210  fmfnfmlem4  24212  clssubg  24364  tgphaus  24372  qustgplem  24376  ucnprima  24536  ucncn  24539  xmeter  24688  imasf1oxms  24744  metustss  24806  metustexhalf  24811  metustfbas  24812  cfilucfil  24814  metuel2  24820  restmetu  24825  mbfconstlem  25884  i1fima  25935  i1fima2  25936  i1fd  25938  itg1addlem5  25957  plyeq0lem  26465  dgrcl  26488  dgrub  26489  dgrlb  26491  vieta1lem1  26571  vieta1lem2  26572  pserulm  26687  psercn2  26688  psercnlem2  26689  psercnlem1  26690  psercn  26691  pserdvlem1  26692  pserdvlem2  26693  pserdv  26694  pserdv2  26695  abelth  26706  eff1olem  26814  dvlog  26917  logtayl  26926  cxpcn3lem  27013  cxpcn3  27014  resqrtcn  27015  basellem5  27350  elnlfn  32438  nlelshi  32570  xppreima  33147  ofpreima  33167  ofpreima2  33168  fnpreimac  33172  ffsrn  33228  indpreima  33340  indf1ofs  33341  pwrssmgc  33469  elrgspnsubrunlem2  33717  elrspunidl  33886  ply1degltel  34034  ply1degleel  34035  ply1degltlss  34036  esplysply  34111  dimkerim  34167  lvecendof1f1o  34173  locfinreflem  34380  zarcmplem  34421  carsggect  34859  sibfof  34881  sitgclg  34883  eulerpartlemsv2  34899  eulerpartlemsf  34900  eulerpartlemv  34905  eulerpartlemb  34909  eulerpartlemt  34912  eulerpartlemr  34915  eulerpartlemgu  34918  eulerpartlemgs2  34921  eulerpartlemn  34922  onvfowev  35743  cvmliftmolem1  35890  cvmlift2lem9  35920  cvmlift3lem6  35933  cvmlift3lem7  35934  mthmsta  36187  dvtan  38433  itg2addnclem  38434  ftc1anclem6  38461  sstotbnd2  38538  keridl  38796  diaintclN  41945  dibintclN  42054  dihintcl  42231  pw2f1ocnv  43892  dnnumch3lem  43901  dnnumch3  43902  pwfi2f1o  43951  binomcxplemdvbinom  45191  binomcxplemdvsum  45193  binomcxplemnotnn0  45194  wessf1ornlem  46031  sge0f1o  47224  mbfresmf  47581  smfco  47644  smfsuplem1  47653  fcores  47969  3f1oss1  47977  uniimaprimaeqfv  48296  elsetpreimafvssdm  48300  gricrel  48849  grlicrel  48936