Theorem cnvimass 5355

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 5346	. 2 |- ( `' A " B ) C_ ran `' A
2		dfdm4 5193	. 2 |- dom A = ran `' A
3	1, 2	sseqtr4i 3537	1 |- ( `' A " B ) C_ dom A

Syntax hints:   C_ wss 3476   `'ccnv 4998   dom cdm 4999   ran crn 5000   "cima 5002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-cnv 5007  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012

This theorem is referenced by:  fvimacnvi  5993  elpreima  5999  iinpreima  6009  fconst4  6123  frnsuppeq  6910  pw2f1olem  7618  cnvimamptfin  7817  fisuppfi  7833  wemapso2OLD  7973  cantnfclOLD  8112  cantnfleOLD  8116  cantnfltOLD  8117  cantnfp1lem2OLD  8120  cantnfp1lem3OLD  8121  cantnflem1bOLD  8124  cantnflem1dOLD  8126  cantnflem1OLD  8127  cantnflem3OLD  8128  cnfcomlemOLD  8147  cnfcomOLD  8148  cnfcom2lemOLD  8149  cnfcom3lemOLD  8151  cnfcom3OLD  8152  infxpenlem  8387  enfin2i  8697  fin1a2lem7  8782  smobeth  8957  fpwwe2lem3  9007  fpwwe2lem12  9015  fpwwe2lem13  9016  fpwwe2  9017  canth4  9021  canthwelem  9024  pwfseqlem4  9036  recmulnq  9338  dmrecnq  9342  nn0suppOLD  10846  ltweuz  12036  isercolllem2  13447  isercolllem3  13448  fsumss  13506  ackbijnn  13599  1arith  14300  vdwlem1  14354  vdwlem5  14358  vdwlem6  14359  vdwlem8  14361  vdwlem11  14364  ghmpreima  16083  gicer  16119  torsubg  16653  gsumval3OLD  16699  gsumzresOLD  16709  gsumzclOLD  16710  gsumzf1oOLD  16711  gsumzaddlemOLD  16727  gsumzmhm  16748  gsumzmhmOLD  16749  gsumzoppg  16758  gsumzoppgOLD  16759  gsum2dOLD  16791  dpjidclOLD  16904  lmhmpreima  17477  mplcoe5  17902  mplcoe2OLD  17904  psr1baslem  17995  evpmss  18389  ofco2  18720  cnpnei  19531  cnclima  19535  iscncl  19536  cnntri  19538  cnclsi  19539  cncls2  19540  cncls  19541  cnntr  19542  cncnp  19547  cnrest2  19553  cndis  19558  2ndcomap  19725  kgencn  19792  kgencn3  19794  ptbasfi  19817  txcnmpt  19860  txdis1cn  19871  qtopval2  19932  basqtop  19947  qtopcld  19949  qtopcn  19950  qtopeu  19952  qtoprest  19953  hmeoimaf1o  20006  hmphtop  20014  hmpher  20020  ordthmeolem  20037  elfm3  20186  rnelfmlem  20188  rnelfm  20189  fmfnfmlem2  20191  fmfnfmlem4  20193  clssubg  20342  tgphaus  20350  divstgplem  20354  tsmsgsumOLD  20375  ucnprima  20520  ucncn  20523  xmeter  20671  imasf1oxms  20727  metustssOLD  20791  metustss  20792  metustexhalfOLD  20801  metustexhalf  20802  metustfbasOLD  20803  metustfbas  20804  cfilucfilOLD  20807  cfilucfil  20808  metuel2  20817  restmetu  20825  mbfconstlem  21771  i1fima  21820  i1fima2  21821  i1fd  21823  itg1addlem5  21842  plyeq0lem  22342  dgrcl  22365  dgrub  22366  dgrlb  22368  vieta1lem1  22440  vieta1lem2  22441  pserulm  22551  psercn2  22552  psercnlem2  22553  psercnlem1  22554  psercn  22555  pserdvlem1  22556  pserdvlem2  22557  pserdv  22558  pserdv2  22559  abelth  22570  eff1olem  22668  dvlog  22760  logtayl  22769  cxpcn3lem  22849  cxpcn3  22850  resqrtcn  22851  basellem5  23086  elnlfn  26523  nlelshi  26655  xppreima  27159  ofpreima  27179  ofpreima2  27180  ffsrn  27224  indpreima  27678  indf1ofs  27679  sibfof  27922  sitgclg  27924  eulerpartlemsv2  27937  eulerpartlemsf  27938  eulerpartlemv  27943  eulerpartlemb  27947  eulerpartlemt  27950  eulerpartlemr  27953  eulerpartlemgu  27956  eulerpartlemgs2  27959  eulerpartlemn  27960  cvmliftmolem1  28366  cvmlift2lem9  28396  cvmlift3lem6  28409  cvmlift3lem7  28410  fprodss  28657  dvtan  29642  itg2addnclem  29643  ftc1anclem6  29672  sstotbnd2  29873  keridl  30032  pw2f1ocnv  30583  dnnumch3lem  30596  dnnumch3  30597  fsuppeq  30647  pwfi2f1o  30648  diaintclN  35855  dibintclN  35964  dihintcl  36141