Theorem cnvimass 5978

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

Syntax hints:   ⊆ wss 3883  ^◡ccnv 5579  dom cdm 5580  ran crn 5581   “ cima 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593

This theorem is referenced by:  cnvimassrndm  6044  fvimacnvi  6911  elpreima  6917  cnvimainrn  6926  iinpreima  6928  rescnvimafod  6933  fconst4  7072  frnsuppeq  7962  frnsuppeqg  7963  pw2f1olem  8816  cnvimamptfin  9050  fisuppfi  9066  infxpenlem  9700  enfin2i  10008  fin1a2lem7  10093  smobeth  10273  fpwwe2lem3  10320  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  canth4  10334  canthwelem  10337  pwfseqlem4  10349  recmulnq  10651  dmrecnq  10655  ltweuz  13609  isercolllem2  15305  isercolllem3  15306  fsumss  15365  ackbijnn  15468  fprodss  15586  1arith  16556  vdwlem1  16610  vdwlem5  16614  vdwlem6  16615  vdwlem8  16617  vdwlem11  16620  ghmpreima  18771  gicer  18807  torsubg  19370  gsumzmhm  19453  gsumzoppg  19460  lmhmpreima  20225  evpmss  20703  mplcoe5  21151  psr1baslem  21266  ofco2  21508  cnpnei  22323  cnclima  22327  iscncl  22328  cnntri  22330  cnclsi  22331  cncls2  22332  cncls  22333  cnntr  22334  cncnp  22339  cnrest2  22345  cndis  22350  2ndcomap  22517  kgencn  22615  kgencn3  22617  ptbasfi  22640  txcnmpt  22683  txdis1cn  22694  qtopval2  22755  basqtop  22770  qtopcld  22772  qtopcn  22773  qtopeu  22775  qtoprest  22776  hmeoimaf1o  22829  hmphtop  22837  hmpher  22843  ordthmeolem  22860  elfm3  23009  rnelfmlem  23011  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem4  23016  clssubg  23168  tgphaus  23176  qustgplem  23180  ucnprima  23342  ucncn  23345  xmeter  23494  imasf1oxms  23551  metustss  23613  metustexhalf  23618  metustfbas  23619  cfilucfil  23621  metuel2  23627  restmetu  23632  mbfconstlem  24696  i1fima  24747  i1fima2  24748  i1fd  24750  itg1addlem5  24770  plyeq0lem  25276  dgrcl  25299  dgrub  25300  dgrlb  25302  vieta1lem1  25375  vieta1lem2  25376  pserulm  25486  psercn2  25487  psercnlem2  25488  psercnlem1  25489  psercn  25490  pserdvlem1  25491  pserdvlem2  25492  pserdv  25493  pserdv2  25494  abelth  25505  eff1olem  25609  dvlog  25711  logtayl  25720  cxpcn3lem  25805  cxpcn3  25806  resqrtcn  25807  basellem5  26139  elnlfn  30191  nlelshi  30323  xppreima  30884  ofpreima  30904  ofpreima2  30905  fnpreimac  30910  ffsrn  30966  pwrssmgc  31180  rhmpreimaidl  31505  elrspunidl  31508  dimkerim  31610  locfinreflem  31692  zarcmplem  31733  indpreima  31893  indf1ofs  31894  carsggect  32185  sibfof  32207  sitgclg  32209  eulerpartlemsv2  32225  eulerpartlemsf  32226  eulerpartlemv  32231  eulerpartlemb  32235  eulerpartlemt  32238  eulerpartlemr  32241  eulerpartlemgu  32244  eulerpartlemgs2  32247  eulerpartlemn  32248  cvmliftmolem1  33143  cvmlift2lem9  33173  cvmlift3lem6  33186  cvmlift3lem7  33187  mthmsta  33440  dvtan  35754  itg2addnclem  35755  ftc1anclem6  35782  sstotbnd2  35859  keridl  36117  diaintclN  38999  dibintclN  39108  dihintcl  39285  pw2f1ocnv  40775  dnnumch3lem  40787  dnnumch3  40788  pwfi2f1o  40837  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  wessf1ornlem  42611  sge0f1o  43810  mbfresmf  44162  smfco  44223  smfsuplem1  44231  fcores  44448  uniimaprimaeqfv  44722  elsetpreimafvssdm  44726