Theorem cnvimass 5984

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

Syntax hints:   ⊆ wss 3888  ^◡ccnv 5585  dom cdm 5586  ran crn 5587   “ cima 5589

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

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 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-br 5076  df-opab 5138  df-xp 5592  df-cnv 5594  df-dm 5596  df-rn 5597  df-res 5598  df-ima 5599

This theorem is referenced by:  cnvimassrndm  6050  fvimacnvi  6923  elpreima  6929  cnvimainrn  6938  iinpreima  6940  rescnvimafod  6945  fconst4  7084  frnsuppeq  7980  frnsuppeqg  7981  pw2f1olem  8852  cnvimamptfin  9109  fisuppfi  9125  infxpenlem  9758  enfin2i  10066  fin1a2lem7  10151  smobeth  10331  fpwwe2lem3  10378  fpwwe2lem11  10386  fpwwe2lem12  10387  fpwwe2  10388  canth4  10392  canthwelem  10395  pwfseqlem4  10407  recmulnq  10709  dmrecnq  10713  ltweuz  13670  isercolllem2  15366  isercolllem3  15367  fsumss  15426  ackbijnn  15529  fprodss  15647  1arith  16617  vdwlem1  16671  vdwlem5  16675  vdwlem6  16676  vdwlem8  16678  vdwlem11  16681  ghmpreima  18845  gicer  18881  torsubg  19444  gsumzmhm  19527  gsumzoppg  19534  lmhmpreima  20299  evpmss  20780  mplcoe5  21230  psr1baslem  21345  ofco2  21589  cnpnei  22404  cnclima  22408  iscncl  22409  cnntri  22411  cnclsi  22412  cncls2  22413  cncls  22414  cnntr  22415  cncnp  22420  cnrest2  22426  cndis  22431  2ndcomap  22598  kgencn  22696  kgencn3  22698  ptbasfi  22721  txcnmpt  22764  txdis1cn  22775  qtopval2  22836  basqtop  22851  qtopcld  22853  qtopcn  22854  qtopeu  22856  qtoprest  22857  hmeoimaf1o  22910  hmphtop  22918  hmpher  22924  ordthmeolem  22941  elfm3  23090  rnelfmlem  23092  rnelfm  23093  fmfnfmlem2  23095  fmfnfmlem4  23097  clssubg  23249  tgphaus  23257  qustgplem  23261  ucnprima  23423  ucncn  23426  xmeter  23575  imasf1oxms  23634  metustss  23696  metustexhalf  23701  metustfbas  23702  cfilucfil  23704  metuel2  23710  restmetu  23715  mbfconstlem  24780  i1fima  24831  i1fima2  24832  i1fd  24834  itg1addlem5  24854  plyeq0lem  25360  dgrcl  25383  dgrub  25384  dgrlb  25386  vieta1lem1  25459  vieta1lem2  25460  pserulm  25570  psercn2  25571  psercnlem2  25572  psercnlem1  25573  psercn  25574  pserdvlem1  25575  pserdvlem2  25576  pserdv  25577  pserdv2  25578  abelth  25589  eff1olem  25693  dvlog  25795  logtayl  25804  cxpcn3lem  25889  cxpcn3  25890  resqrtcn  25891  basellem5  26223  elnlfn  30277  nlelshi  30409  xppreima  30970  ofpreima  30989  ofpreima2  30990  fnpreimac  30995  ffsrn  31051  pwrssmgc  31265  rhmpreimaidl  31590  elrspunidl  31593  dimkerim  31695  locfinreflem  31777  zarcmplem  31818  indpreima  31980  indf1ofs  31981  carsggect  32272  sibfof  32294  sitgclg  32296  eulerpartlemsv2  32312  eulerpartlemsf  32313  eulerpartlemv  32318  eulerpartlemb  32322  eulerpartlemt  32325  eulerpartlemr  32328  eulerpartlemgu  32331  eulerpartlemgs2  32334  eulerpartlemn  32335  cvmliftmolem1  33230  cvmlift2lem9  33260  cvmlift3lem6  33273  cvmlift3lem7  33274  mthmsta  33527  dvtan  35814  itg2addnclem  35815  ftc1anclem6  35842  sstotbnd2  35919  keridl  36177  diaintclN  39059  dibintclN  39168  dihintcl  39345  pw2f1ocnv  40846  dnnumch3lem  40858  dnnumch3  40859  pwfi2f1o  40908  binomcxplemdvbinom  41931  binomcxplemdvsum  41933  binomcxplemnotnn0  41934  wessf1ornlem  42682  sge0f1o  43880  mbfresmf  44232  smfco  44293  smfsuplem1  44301  fcores  44518  uniimaprimaeqfv  44791  elsetpreimafvssdm  44795