Theorem cnvimass 5187

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

Syntax hints:   C_ wss 3403   `'ccnv 4832   dom cdm 4833   ran crn 4834   "cima 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-xp 4839  df-cnv 4841  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846

This theorem is referenced by:  fvimacnvi  5994  elpreima  6000  iinpreima  6008  fconst4  6127  frnsuppeq  6923  pw2f1olem  7673  cnvimamptfin  7872  fisuppfi  7888  infxpenlem  8441  enfin2i  8748  fin1a2lem7  8833  smobeth  9008  fpwwe2lem3  9055  fpwwe2lem12  9063  fpwwe2lem13  9064  fpwwe2  9065  canth4  9069  canthwelem  9072  pwfseqlem4  9084  recmulnq  9386  dmrecnq  9390  ltweuz  12172  isercolllem2  13722  isercolllem3  13723  fsumss  13784  ackbijnn  13879  fprodss  13995  1arith  14864  vdwlem1  14924  vdwlem5  14928  vdwlem6  14929  vdwlem8  14931  vdwlem11  14934  ghmpreima  16897  gicer  16933  torsubg  17485  gsumzmhm  17563  gsumzoppg  17570  lmhmpreima  18264  mplcoe5  18685  psr1baslem  18771  evpmss  19147  ofco2  19469  cnpnei  20273  cnclima  20277  iscncl  20278  cnntri  20280  cnclsi  20281  cncls2  20282  cncls  20283  cnntr  20284  cncnp  20289  cnrest2  20295  cndis  20300  2ndcomap  20466  kgencn  20564  kgencn3  20566  ptbasfi  20589  txcnmpt  20632  txdis1cn  20643  qtopval2  20704  basqtop  20719  qtopcld  20721  qtopcn  20722  qtopeu  20724  qtoprest  20725  hmeoimaf1o  20778  hmphtop  20786  hmpher  20792  ordthmeolem  20809  elfm3  20958  rnelfmlem  20960  rnelfm  20961  fmfnfmlem2  20963  fmfnfmlem4  20965  clssubg  21116  tgphaus  21124  qustgplem  21128  ucnprima  21290  ucncn  21293  xmeter  21441  imasf1oxms  21497  metustss  21559  metustexhalf  21564  metustfbas  21565  cfilucfil  21567  metuel2  21573  restmetu  21578  mbfconstlem  22578  i1fima  22629  i1fima2  22630  i1fd  22632  itg1addlem5  22651  plyeq0lem  23157  dgrcl  23180  dgrub  23181  dgrlb  23183  vieta1lem1  23256  vieta1lem2  23257  pserulm  23370  psercn2  23371  psercnlem2  23372  psercnlem1  23373  psercn  23374  pserdvlem1  23375  pserdvlem2  23376  pserdv  23377  pserdv2  23378  abelth  23389  eff1olem  23490  dvlog  23589  logtayl  23598  cxpcn3lem  23680  cxpcn3  23681  resqrtcn  23682  basellem5  24004  elnlfn  27574  nlelshi  27706  xppreima  28241  ofpreima  28261  ofpreima2  28262  ffsrn  28307  locfinreflem  28660  indpreima  28839  indf1ofs  28840  carsggect  29143  sibfof  29166  sitgclg  29168  eulerpartlemsv2  29184  eulerpartlemsf  29185  eulerpartlemv  29190  eulerpartlemb  29194  eulerpartlemt  29197  eulerpartlemr  29200  eulerpartlemgu  29203  eulerpartlemgs2  29206  eulerpartlemn  29207  cvmliftmolem1  29997  cvmlift2lem9  30027  cvmlift3lem6  30040  cvmlift3lem7  30041  mthmsta  30209  dvtan  31985  itg2addnclem  31986  ftc1anclem6  32015  sstotbnd2  32099  keridl  32258  diaintclN  34620  dibintclN  34729  dihintcl  34906  pw2f1ocnv  35886  dnnumch3lem  35898  dnnumch3  35899  pwfi2f1o  35948  binomcxplemdvbinom  36696  binomcxplemdvsum  36698  binomcxplemnotnn0  36699  wessf1ornlem  37453  sge0f1o  38218