Theorem cnvimass 6074

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

Syntax hints:   ⊆ wss 3931  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   “ cima 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is referenced by:  cnvimassrndm  6146  fvimacnvi  7047  elpreima  7053  cnvimainrn  7062  iinpreima  7064  rescnvimafod  7068  fconst4  7211  fsuppeq  8179  fsuppeqg  8180  pw2f1olem  9095  cnvimamptfin  9370  fisuppfi  9388  infxpenlem  10032  enfin2i  10340  fin1a2lem7  10425  smobeth  10605  fpwwe2lem3  10652  fpwwe2lem11  10660  fpwwe2lem12  10661  fpwwe2  10662  canth4  10666  canthwelem  10669  pwfseqlem4  10681  recmulnq  10983  dmrecnq  10987  ltweuz  13984  isercolllem2  15687  isercolllem3  15688  fsumss  15746  ackbijnn  15849  fprodss  15969  1arith  16952  vdwlem1  17006  vdwlem5  17010  vdwlem6  17011  vdwlem8  17013  vdwlem11  17016  ghmpreima  19226  gicer  19265  torsubg  19840  gsumzmhm  19923  gsumzoppg  19930  lmhmpreima  21011  rhmpreimaidl  21243  evpmss  21551  mplcoe5  22003  psr1baslem  22125  ofco2  22394  cnpnei  23207  cnclima  23211  iscncl  23212  cnntri  23214  cnclsi  23215  cncls2  23216  cncls  23217  cnntr  23218  cncnp  23223  cnrest2  23229  cndis  23234  2ndcomap  23401  kgencn  23499  kgencn3  23501  ptbasfi  23524  txcnmpt  23567  txdis1cn  23578  qtopval2  23639  basqtop  23654  qtopcld  23656  qtopcn  23657  qtopeu  23659  qtoprest  23660  hmeoimaf1o  23713  hmphtop  23721  hmpher  23727  ordthmeolem  23744  elfm3  23893  rnelfmlem  23895  rnelfm  23896  fmfnfmlem2  23898  fmfnfmlem4  23900  clssubg  24052  tgphaus  24060  qustgplem  24064  ucnprima  24225  ucncn  24228  xmeter  24377  imasf1oxms  24433  metustss  24495  metustexhalf  24500  metustfbas  24501  cfilucfil  24503  metuel2  24509  restmetu  24514  mbfconstlem  25585  i1fima  25636  i1fima2  25637  i1fd  25639  itg1addlem5  25658  plyeq0lem  26172  dgrcl  26195  dgrub  26196  dgrlb  26198  vieta1lem1  26275  vieta1lem2  26276  pserulm  26388  psercn2  26389  psercn2OLD  26390  psercnlem2  26391  psercnlem1  26392  psercn  26393  pserdvlem1  26394  pserdvlem2  26395  pserdv  26396  pserdv2  26397  abelth  26408  eff1olem  26514  dvlog  26617  logtayl  26626  cxpcn3lem  26714  cxpcn3  26715  resqrtcn  26716  basellem5  27052  elnlfn  31914  nlelshi  32046  xppreima  32628  ofpreima  32648  ofpreima2  32649  fnpreimac  32654  ffsrn  32711  indpreima  32847  indf1ofs  32848  pwrssmgc  32985  elrgspnsubrunlem2  33248  elrspunidl  33448  ply1degltel  33609  ply1degleel  33610  ply1degltlss  33611  dimkerim  33672  lvecendof1f1o  33678  locfinreflem  33876  zarcmplem  33917  carsggect  34355  sibfof  34377  sitgclg  34379  eulerpartlemsv2  34395  eulerpartlemsf  34396  eulerpartlemv  34401  eulerpartlemb  34405  eulerpartlemt  34408  eulerpartlemr  34411  eulerpartlemgu  34414  eulerpartlemgs2  34417  eulerpartlemn  34418  cvmliftmolem1  35308  cvmlift2lem9  35338  cvmlift3lem6  35351  cvmlift3lem7  35352  mthmsta  35605  dvtan  37699  itg2addnclem  37700  ftc1anclem6  37727  sstotbnd2  37803  keridl  38061  diaintclN  41082  dibintclN  41191  dihintcl  41368  pw2f1ocnv  43036  dnnumch3lem  43045  dnnumch3  43046  pwfi2f1o  43095  binomcxplemdvbinom  44352  binomcxplemdvsum  44354  binomcxplemnotnn0  44355  wessf1ornlem  45189  sge0f1o  46391  mbfresmf  46748  smfco  46811  smfsuplem1  46820  fcores  47076  3f1oss1  47084  uniimaprimaeqfv  47376  elsetpreimafvssdm  47380  gricrel  47912  grlicrel  47991