Theorem cnvimass 6039

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

Syntax hints:   ⊆ wss 3890  ^◡ccnv 5621  dom cdm 5622  ran crn 5623   “ cima 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5628  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635

This theorem is referenced by:  cnvimassrndm  6108  fvimacnvi  6996  elpreima  7002  cnvimainrn  7011  iinpreima  7013  rescnvimafod  7017  fconst4  7160  fsuppeq  8116  fsuppeqg  8117  pw2f1olem  9010  cnvimamptfin  9254  fisuppfi  9275  infxpenlem  9924  enfin2i  10232  fin1a2lem7  10317  smobeth  10498  fpwwe2lem3  10545  fpwwe2lem11  10553  fpwwe2lem12  10554  fpwwe2  10555  canth4  10559  canthwelem  10562  pwfseqlem4  10574  recmulnq  10876  dmrecnq  10880  ltweuz  13912  isercolllem2  15617  isercolllem3  15618  fsumss  15676  ackbijnn  15782  fprodss  15902  1arith  16887  vdwlem1  16941  vdwlem5  16945  vdwlem6  16946  vdwlem8  16948  vdwlem11  16951  ghmpreima  19202  gicer  19241  torsubg  19818  gsumzmhm  19901  gsumzoppg  19908  lmhmpreima  21033  rhmpreimaidl  21265  evpmss  21574  mplcoe5  22027  psr1baslem  22157  ofco2  22425  cnpnei  23238  cnclima  23242  iscncl  23243  cnntri  23245  cnclsi  23246  cncls2  23247  cncls  23248  cnntr  23249  cncnp  23254  cnrest2  23260  cndis  23265  2ndcomap  23432  kgencn  23530  kgencn3  23532  ptbasfi  23555  txcnmpt  23598  txdis1cn  23609  qtopval2  23670  basqtop  23685  qtopcld  23687  qtopcn  23688  qtopeu  23690  qtoprest  23691  hmeoimaf1o  23744  hmphtop  23752  hmpher  23758  ordthmeolem  23775  elfm3  23924  rnelfmlem  23926  rnelfm  23927  fmfnfmlem2  23929  fmfnfmlem4  23931  clssubg  24083  tgphaus  24091  qustgplem  24095  ucnprima  24255  ucncn  24258  xmeter  24407  imasf1oxms  24463  metustss  24525  metustexhalf  24530  metustfbas  24531  cfilucfil  24533  metuel2  24539  restmetu  24544  mbfconstlem  25603  i1fima  25654  i1fima2  25655  i1fd  25657  itg1addlem5  25676  plyeq0lem  26187  dgrcl  26210  dgrub  26211  dgrlb  26213  vieta1lem1  26289  vieta1lem2  26290  pserulm  26402  psercn2  26403  psercn2OLD  26404  psercnlem2  26405  psercnlem1  26406  psercn  26407  pserdvlem1  26408  pserdvlem2  26409  pserdv  26410  pserdv2  26411  abelth  26422  eff1olem  26528  dvlog  26631  logtayl  26640  cxpcn3lem  26728  cxpcn3  26729  resqrtcn  26730  basellem5  27066  elnlfn  32019  nlelshi  32151  xppreima  32738  ofpreima  32758  ofpreima2  32759  fnpreimac  32763  ffsrn  32821  indpreima  32945  indf1ofs  32946  pwrssmgc  33080  elrgspnsubrunlem2  33329  elrspunidl  33508  ply1degltel  33674  ply1degleel  33675  ply1degltlss  33676  esplysply  33735  dimkerim  33792  lvecendof1f1o  33798  locfinreflem  34005  zarcmplem  34046  carsggect  34483  sibfof  34505  sitgclg  34507  eulerpartlemsv2  34523  eulerpartlemsf  34524  eulerpartlemv  34529  eulerpartlemb  34533  eulerpartlemt  34536  eulerpartlemr  34539  eulerpartlemgu  34542  eulerpartlemgs2  34545  eulerpartlemn  34546  cvmliftmolem1  35484  cvmlift2lem9  35514  cvmlift3lem6  35527  cvmlift3lem7  35528  mthmsta  35781  dvtan  38002  itg2addnclem  38003  ftc1anclem6  38030  sstotbnd2  38106  keridl  38364  diaintclN  41515  dibintclN  41624  dihintcl  41801  pw2f1ocnv  43480  dnnumch3lem  43489  dnnumch3  43490  pwfi2f1o  43539  binomcxplemdvbinom  44795  binomcxplemdvsum  44797  binomcxplemnotnn0  44798  wessf1ornlem  45630  sge0f1o  46825  mbfresmf  47182  smfco  47245  smfsuplem1  47254  fcores  47512  3f1oss1  47520  uniimaprimaeqfv  47839  elsetpreimafvssdm  47843  gricrel  48392  grlicrel  48479