Theorem cnvimass 5199

Description: A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)

Assertion

Ref	Expression
cnvimass	|- ( `' A " B ) C_ dom A

Proof of Theorem cnvimass

Step	Hyp	Ref	Expression
1		imassrn 5190	. 2 |- ( `' A " B ) C_ ran `' A
2		dfdm4 5038	. 2 |- dom A = ran `' A
3	1, 2	sseqtr4i 3494	1 |- ( `' A " B ) C_ dom A

Syntax hints:   C_ wss 3433   `'ccnv 4844   dom cdm 4845   ran crn 4846   "cima 4848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-br 4418  df-opab 4476  df-xp 4851  df-cnv 4853  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858

This theorem is referenced by:  fvimacnvi  6002  elpreima  6008  iinpreima  6016  fconst4  6135  frnsuppeq  6928  pw2f1olem  7673  cnvimamptfin  7872  fisuppfi  7888  infxpenlem  8434  enfin2i  8740  fin1a2lem7  8825  smobeth  9000  fpwwe2lem3  9047  fpwwe2lem12  9055  fpwwe2lem13  9056  fpwwe2  9057  canth4  9061  canthwelem  9064  pwfseqlem4  9076  recmulnq  9378  dmrecnq  9382  ltweuz  12161  isercolllem2  13696  isercolllem3  13697  fsumss  13758  ackbijnn  13853  fprodss  13969  1arith  14823  vdwlem1  14883  vdwlem5  14887  vdwlem6  14888  vdwlem8  14890  vdwlem11  14893  ghmpreima  16848  gicer  16884  torsubg  17420  gsumzmhm  17498  gsumzoppg  17505  lmhmpreima  18199  mplcoe5  18620  psr1baslem  18706  evpmss  19078  ofco2  19400  cnpnei  20204  cnclima  20208  iscncl  20209  cnntri  20211  cnclsi  20212  cncls2  20213  cncls  20214  cnntr  20215  cncnp  20220  cnrest2  20226  cndis  20231  2ndcomap  20397  kgencn  20495  kgencn3  20497  ptbasfi  20520  txcnmpt  20563  txdis1cn  20574  qtopval2  20635  basqtop  20650  qtopcld  20652  qtopcn  20653  qtopeu  20655  qtoprest  20656  hmeoimaf1o  20709  hmphtop  20717  hmpher  20723  ordthmeolem  20740  elfm3  20889  rnelfmlem  20891  rnelfm  20892  fmfnfmlem2  20894  fmfnfmlem4  20896  clssubg  21047  tgphaus  21055  qustgplem  21059  ucnprima  21221  ucncn  21224  xmeter  21372  imasf1oxms  21428  metustss  21490  metustexhalf  21495  metustfbas  21496  cfilucfil  21498  metuel2  21504  restmetu  21509  mbfconstlem  22459  i1fima  22510  i1fima2  22511  i1fd  22513  itg1addlem5  22532  plyeq0lem  23029  dgrcl  23052  dgrub  23053  dgrlb  23055  vieta1lem1  23128  vieta1lem2  23129  pserulm  23239  psercn2  23240  psercnlem2  23241  psercnlem1  23242  psercn  23243  pserdvlem1  23244  pserdvlem2  23245  pserdv  23246  pserdv2  23247  abelth  23258  eff1olem  23359  dvlog  23458  logtayl  23467  cxpcn3lem  23549  cxpcn3  23550  resqrtcn  23551  basellem5  23871  elnlfn  27413  nlelshi  27545  xppreima  28085  ofpreima  28105  ofpreima2  28106  ffsrn  28154  locfinreflem  28503  indpreima  28682  indf1ofs  28683  carsggect  28976  sibfof  28998  sitgclg  29000  eulerpartlemsv2  29014  eulerpartlemsf  29015  eulerpartlemv  29020  eulerpartlemb  29024  eulerpartlemt  29027  eulerpartlemr  29030  eulerpartlemgu  29033  eulerpartlemgs2  29036  eulerpartlemn  29037  cvmliftmolem1  29789  cvmlift2lem9  29819  cvmlift3lem6  29832  cvmlift3lem7  29833  mthmsta  30001  dvtan  31696  itg2addnclem  31697  ftc1anclem6  31726  sstotbnd2  31810  keridl  31969  diaintclN  34335  dibintclN  34444  dihintcl  34621  pw2f1ocnv  35602  dnnumch3lem  35614  dnnumch3  35615  pwfi2f1o  35664  binomcxplemdvbinom  36343  binomcxplemdvsum  36345  binomcxplemnotnn0  36346  wessf1ornlem  37086  sge0f1o  37762