Theorem cnvimass 6053

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

Syntax hints:   ⊆ wss 3914  ^◡ccnv 5637  dom cdm 5638  ran crn 5639   “ cima 5641

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  cnvimassrndm  6125  fvimacnvi  7024  elpreima  7030  cnvimainrn  7039  iinpreima  7041  rescnvimafod  7045  fconst4  7188  fsuppeq  8154  fsuppeqg  8155  pw2f1olem  9045  cnvimamptfin  9304  fisuppfi  9322  infxpenlem  9966  enfin2i  10274  fin1a2lem7  10359  smobeth  10539  fpwwe2lem3  10586  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  canth4  10600  canthwelem  10603  pwfseqlem4  10615  recmulnq  10917  dmrecnq  10921  ltweuz  13926  isercolllem2  15632  isercolllem3  15633  fsumss  15691  ackbijnn  15794  fprodss  15914  1arith  16898  vdwlem1  16952  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  vdwlem11  16962  ghmpreima  19170  gicer  19209  torsubg  19784  gsumzmhm  19867  gsumzoppg  19874  lmhmpreima  20955  rhmpreimaidl  21187  evpmss  21495  mplcoe5  21947  psr1baslem  22069  ofco2  22338  cnpnei  23151  cnclima  23155  iscncl  23156  cnntri  23158  cnclsi  23159  cncls2  23160  cncls  23161  cnntr  23162  cncnp  23167  cnrest2  23173  cndis  23178  2ndcomap  23345  kgencn  23443  kgencn3  23445  ptbasfi  23468  txcnmpt  23511  txdis1cn  23522  qtopval2  23583  basqtop  23598  qtopcld  23600  qtopcn  23601  qtopeu  23603  qtoprest  23604  hmeoimaf1o  23657  hmphtop  23665  hmpher  23671  ordthmeolem  23688  elfm3  23837  rnelfmlem  23839  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem4  23844  clssubg  23996  tgphaus  24004  qustgplem  24008  ucnprima  24169  ucncn  24172  xmeter  24321  imasf1oxms  24377  metustss  24439  metustexhalf  24444  metustfbas  24445  cfilucfil  24447  metuel2  24453  restmetu  24458  mbfconstlem  25528  i1fima  25579  i1fima2  25580  i1fd  25582  itg1addlem5  25601  plyeq0lem  26115  dgrcl  26138  dgrub  26139  dgrlb  26141  vieta1lem1  26218  vieta1lem2  26219  pserulm  26331  psercn2  26332  psercn2OLD  26333  psercnlem2  26334  psercnlem1  26335  psercn  26336  pserdvlem1  26337  pserdvlem2  26338  pserdv  26339  pserdv2  26340  abelth  26351  eff1olem  26457  dvlog  26560  logtayl  26569  cxpcn3lem  26657  cxpcn3  26658  resqrtcn  26659  basellem5  26995  elnlfn  31857  nlelshi  31989  xppreima  32569  ofpreima  32589  ofpreima2  32590  fnpreimac  32595  ffsrn  32652  indpreima  32788  indf1ofs  32789  pwrssmgc  32926  elrgspnsubrunlem2  33199  elrspunidl  33399  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  dimkerim  33623  lvecendof1f1o  33629  locfinreflem  33830  zarcmplem  33871  carsggect  34309  sibfof  34331  sitgclg  34333  eulerpartlemsv2  34349  eulerpartlemsf  34350  eulerpartlemv  34355  eulerpartlemb  34359  eulerpartlemt  34362  eulerpartlemr  34365  eulerpartlemgu  34368  eulerpartlemgs2  34371  eulerpartlemn  34372  cvmliftmolem1  35268  cvmlift2lem9  35298  cvmlift3lem6  35311  cvmlift3lem7  35312  mthmsta  35565  dvtan  37664  itg2addnclem  37665  ftc1anclem6  37692  sstotbnd2  37768  keridl  38026  diaintclN  41052  dibintclN  41161  dihintcl  41338  pw2f1ocnv  43026  dnnumch3lem  43035  dnnumch3  43036  pwfi2f1o  43085  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  wessf1ornlem  45179  sge0f1o  46380  mbfresmf  46737  smfco  46800  smfsuplem1  46809  fcores  47068  3f1oss1  47076  uniimaprimaeqfv  47383  elsetpreimafvssdm  47387  gricrel  47919  grlicrel  47998