Theorem cnvimass 5347

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

Syntax hints:   C_ wss 3461   `'ccnv 4988   dom cdm 4989   ran crn 4990   "cima 4992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-cnv 4997  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002

This theorem is referenced by:  fvimacnvi  5986  elpreima  5992  iinpreima  6002  fconst4  6121  frnsuppeq  6915  pw2f1olem  7623  cnvimamptfin  7823  fisuppfi  7839  wemapso2OLD  7980  cantnfclOLD  8119  cantnfleOLD  8123  cantnfltOLD  8124  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1dOLD  8133  cantnflem1OLD  8134  cantnflem3OLD  8135  cnfcomlemOLD  8154  cnfcomOLD  8155  cnfcom2lemOLD  8156  cnfcom3lemOLD  8158  cnfcom3OLD  8159  infxpenlem  8394  enfin2i  8704  fin1a2lem7  8789  smobeth  8964  fpwwe2lem3  9014  fpwwe2lem12  9022  fpwwe2lem13  9023  fpwwe2  9024  canth4  9028  canthwelem  9031  pwfseqlem4  9043  recmulnq  9345  dmrecnq  9349  nn0suppOLD  10857  ltweuz  12054  isercolllem2  13470  isercolllem3  13471  fsumss  13529  ackbijnn  13622  fprodss  13737  1arith  14427  vdwlem1  14481  vdwlem5  14485  vdwlem6  14486  vdwlem8  14488  vdwlem11  14491  ghmpreima  16267  gicer  16303  torsubg  16839  gsumval3OLD  16887  gsumzresOLD  16897  gsumzclOLD  16898  gsumzf1oOLD  16899  gsumzaddlemOLD  16915  gsumzmhm  16936  gsumzmhmOLD  16937  gsumzoppg  16946  gsumzoppgOLD  16947  gsum2dOLD  16979  dpjidclOLD  17093  lmhmpreima  17673  mplcoe5  18110  mplcoe2OLD  18112  psr1baslem  18203  evpmss  18600  ofco2  18931  cnpnei  19743  cnclima  19747  iscncl  19748  cnntri  19750  cnclsi  19751  cncls2  19752  cncls  19753  cnntr  19754  cncnp  19759  cnrest2  19765  cndis  19770  2ndcomap  19937  kgencn  20035  kgencn3  20037  ptbasfi  20060  txcnmpt  20103  txdis1cn  20114  qtopval2  20175  basqtop  20190  qtopcld  20192  qtopcn  20193  qtopeu  20195  qtoprest  20196  hmeoimaf1o  20249  hmphtop  20257  hmpher  20263  ordthmeolem  20280  elfm3  20429  rnelfmlem  20431  rnelfm  20432  fmfnfmlem2  20434  fmfnfmlem4  20436  clssubg  20585  tgphaus  20593  qustgplem  20597  tsmsgsumOLD  20618  ucnprima  20763  ucncn  20766  xmeter  20914  imasf1oxms  20970  metustssOLD  21034  metustss  21035  metustexhalfOLD  21044  metustexhalf  21045  metustfbasOLD  21046  metustfbas  21047  cfilucfilOLD  21050  cfilucfil  21051  metuel2  21060  restmetu  21068  mbfconstlem  22014  i1fima  22063  i1fima2  22064  i1fd  22066  itg1addlem5  22085  plyeq0lem  22585  dgrcl  22608  dgrub  22609  dgrlb  22611  vieta1lem1  22684  vieta1lem2  22685  pserulm  22795  psercn2  22796  psercnlem2  22797  psercnlem1  22798  psercn  22799  pserdvlem1  22800  pserdvlem2  22801  pserdv  22802  pserdv2  22803  abelth  22814  eff1olem  22913  dvlog  23010  logtayl  23019  cxpcn3lem  23099  cxpcn3  23100  resqrtcn  23101  basellem5  23336  elnlfn  26825  nlelshi  26957  xppreima  27465  ofpreima  27485  ofpreima2  27486  ffsrn  27530  gsummpt2co  27749  locfinreflem  27821  indpreima  28016  indf1ofs  28017  sibfof  28260  sitgclg  28262  eulerpartlemsv2  28275  eulerpartlemsf  28276  eulerpartlemv  28281  eulerpartlemb  28285  eulerpartlemt  28288  eulerpartlemr  28291  eulerpartlemgu  28294  eulerpartlemgs2  28297  eulerpartlemn  28298  cvmliftmolem1  28704  cvmlift2lem9  28734  cvmlift3lem6  28747  cvmlift3lem7  28748  mthmsta  28916  dvtan  30041  itg2addnclem  30042  ftc1anclem6  30071  sstotbnd2  30246  keridl  30405  pw2f1ocnv  30955  dnnumch3lem  30968  dnnumch3  30969  fsuppeq  31019  pwfi2f1o  31020  diaintclN  36660  dibintclN  36769  dihintcl  36946