Theorem cnvimass 5992

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

Syntax hints:   ⊆ wss 3888  ^◡ccnv 5589  dom cdm 5590  ran crn 5591   “ cima 5593

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 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-xp 5596  df-cnv 5598  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603

This theorem is referenced by:  cnvimassrndm  6060  fvimacnvi  6938  elpreima  6944  cnvimainrn  6953  iinpreima  6955  rescnvimafod  6960  fconst4  7099  frnsuppeq  8000  frnsuppeqg  8001  pw2f1olem  8872  cnvimamptfin  9129  fisuppfi  9145  infxpenlem  9778  enfin2i  10086  fin1a2lem7  10171  smobeth  10351  fpwwe2lem3  10398  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  canth4  10412  canthwelem  10415  pwfseqlem4  10427  recmulnq  10729  dmrecnq  10733  ltweuz  13690  isercolllem2  15386  isercolllem3  15387  fsumss  15446  ackbijnn  15549  fprodss  15667  1arith  16637  vdwlem1  16691  vdwlem5  16695  vdwlem6  16696  vdwlem8  16698  vdwlem11  16701  ghmpreima  18865  gicer  18901  torsubg  19464  gsumzmhm  19547  gsumzoppg  19554  lmhmpreima  20319  evpmss  20800  mplcoe5  21250  psr1baslem  21365  ofco2  21609  cnpnei  22424  cnclima  22428  iscncl  22429  cnntri  22431  cnclsi  22432  cncls2  22433  cncls  22434  cnntr  22435  cncnp  22440  cnrest2  22446  cndis  22451  2ndcomap  22618  kgencn  22716  kgencn3  22718  ptbasfi  22741  txcnmpt  22784  txdis1cn  22795  qtopval2  22856  basqtop  22871  qtopcld  22873  qtopcn  22874  qtopeu  22876  qtoprest  22877  hmeoimaf1o  22930  hmphtop  22938  hmpher  22944  ordthmeolem  22961  elfm3  23110  rnelfmlem  23112  rnelfm  23113  fmfnfmlem2  23115  fmfnfmlem4  23117  clssubg  23269  tgphaus  23277  qustgplem  23281  ucnprima  23443  ucncn  23446  xmeter  23595  imasf1oxms  23654  metustss  23716  metustexhalf  23721  metustfbas  23722  cfilucfil  23724  metuel2  23730  restmetu  23735  mbfconstlem  24800  i1fima  24851  i1fima2  24852  i1fd  24854  itg1addlem5  24874  plyeq0lem  25380  dgrcl  25403  dgrub  25404  dgrlb  25406  vieta1lem1  25479  vieta1lem2  25480  pserulm  25590  psercn2  25591  psercnlem2  25592  psercnlem1  25593  psercn  25594  pserdvlem1  25595  pserdvlem2  25596  pserdv  25597  pserdv2  25598  abelth  25609  eff1olem  25713  dvlog  25815  logtayl  25824  cxpcn3lem  25909  cxpcn3  25910  resqrtcn  25911  basellem5  26243  elnlfn  30299  nlelshi  30431  xppreima  30992  ofpreima  31011  ofpreima2  31012  fnpreimac  31017  ffsrn  31073  pwrssmgc  31287  rhmpreimaidl  31612  elrspunidl  31615  dimkerim  31717  locfinreflem  31799  zarcmplem  31840  indpreima  32002  indf1ofs  32003  carsggect  32294  sibfof  32316  sitgclg  32318  eulerpartlemsv2  32334  eulerpartlemsf  32335  eulerpartlemv  32340  eulerpartlemb  32344  eulerpartlemt  32347  eulerpartlemr  32350  eulerpartlemgu  32353  eulerpartlemgs2  32356  eulerpartlemn  32357  cvmliftmolem1  33252  cvmlift2lem9  33282  cvmlift3lem6  33295  cvmlift3lem7  33296  mthmsta  33549  dvtan  35836  itg2addnclem  35837  ftc1anclem6  35864  sstotbnd2  35941  keridl  36199  diaintclN  39079  dibintclN  39188  dihintcl  39365  pw2f1ocnv  40866  dnnumch3lem  40878  dnnumch3  40879  pwfi2f1o  40928  binomcxplemdvbinom  41978  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  wessf1ornlem  42729  sge0f1o  43927  mbfresmf  44284  smfco  44347  smfsuplem1  44355  fcores  44572  uniimaprimaeqfv  44845  elsetpreimafvssdm  44849