Theorem cnvimass 5204

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

Syntax hints:   C_ wss 3343   `'ccnv 4854   dom cdm 4855   ran crn 4856   "cima 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pr 4546

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2735  df-rex 2736  df-rab 2739  df-v 2989  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-br 4308  df-opab 4366  df-xp 4861  df-cnv 4863  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868

This theorem is referenced by:  fvimacnvi  5832  elpreima  5838  iinpreima  5848  fconst4  5957  frnsuppeq  6717  pw2f1olem  7430  cnvimamptfin  7627  fisuppfi  7643  wemapso2OLD  7781  cantnfclOLD  7920  cantnfleOLD  7924  cantnfltOLD  7925  cantnfp1lem2OLD  7928  cantnfp1lem3OLD  7929  cantnflem1bOLD  7932  cantnflem1dOLD  7934  cantnflem1OLD  7935  cantnflem3OLD  7936  cnfcomlemOLD  7955  cnfcomOLD  7956  cnfcom2lemOLD  7957  cnfcom3lemOLD  7959  cnfcom3OLD  7960  infxpenlem  8195  enfin2i  8505  fin1a2lem7  8590  smobeth  8765  fpwwe2lem3  8815  fpwwe2lem12  8823  fpwwe2lem13  8824  fpwwe2  8825  canth4  8829  canthwelem  8832  pwfseqlem4  8844  recmulnq  9148  dmrecnq  9152  nn0suppOLD  10649  ltweuz  11799  isercolllem2  13158  isercolllem3  13159  fsumss  13217  ackbijnn  13306  1arith  14003  vdwlem1  14057  vdwlem5  14061  vdwlem6  14062  vdwlem8  14064  vdwlem11  14067  ghmpreima  15783  gicer  15819  torsubg  16351  gsumval3OLD  16397  gsumzresOLD  16407  gsumzclOLD  16408  gsumzf1oOLD  16409  gsumzaddlemOLD  16425  gsumzmhm  16445  gsumzmhmOLD  16446  gsumzoppg  16455  gsumzoppgOLD  16456  gsum2dOLD  16479  dpjidclOLD  16579  lmhmpreima  17144  mplcoe5  17563  mplcoe2OLD  17565  psr1baslem  17656  evpmss  18031  ofco2  18347  cnpnei  18883  cnclima  18887  iscncl  18888  cnntri  18890  cnclsi  18891  cncls2  18892  cncls  18893  cnntr  18894  cncnp  18899  cnrest2  18905  cndis  18910  2ndcomap  19077  kgencn  19144  kgencn3  19146  ptbasfi  19169  txcnmpt  19212  txdis1cn  19223  qtopval2  19284  basqtop  19299  qtopcld  19301  qtopcn  19302  qtopeu  19304  qtoprest  19305  hmeoimaf1o  19358  hmphtop  19366  hmpher  19372  ordthmeolem  19389  elfm3  19538  rnelfmlem  19540  rnelfm  19541  fmfnfmlem2  19543  fmfnfmlem4  19545  clssubg  19694  tgphaus  19702  divstgplem  19706  tsmsgsumOLD  19727  ucnprima  19872  ucncn  19875  xmeter  20023  imasf1oxms  20079  metustssOLD  20143  metustss  20144  metustexhalfOLD  20153  metustexhalf  20154  metustfbasOLD  20155  metustfbas  20156  cfilucfilOLD  20159  cfilucfil  20160  metuel2  20169  restmetu  20177  mbfconstlem  21122  i1fima  21171  i1fima2  21172  i1fd  21174  itg1addlem5  21193  plyeq0lem  21693  dgrcl  21716  dgrub  21717  dgrlb  21719  vieta1lem1  21791  vieta1lem2  21792  pserulm  21902  psercn2  21903  psercnlem2  21904  psercnlem1  21905  psercn  21906  pserdvlem1  21907  pserdvlem2  21908  pserdv  21909  pserdv2  21910  abelth  21921  eff1olem  22019  dvlog  22111  logtayl  22120  cxpcn3lem  22200  cxpcn3  22201  resqrcn  22202  basellem5  22437  elnlfn  25347  nlelshi  25479  xppreima  25979  ofpreima  25999  ofpreima2  26000  ffsrn  26044  gsumunsnf  26260  gsumle  26261  indpreima  26496  indf1ofs  26497  sibfof  26741  sitgclg  26743  eulerpartlemsv2  26756  eulerpartlemsf  26757  eulerpartlemv  26762  eulerpartlemb  26766  eulerpartlemt  26769  eulerpartlemr  26772  eulerpartlemgu  26775  eulerpartlemgs2  26778  eulerpartlemn  26779  cvmliftmolem1  27185  cvmlift2lem9  27215  cvmlift3lem6  27228  cvmlift3lem7  27229  fprodss  27476  dvtan  28461  itg2addnclem  28462  ftc1anclem6  28491  sstotbnd2  28692  keridl  28851  pw2f1ocnv  29405  dnnumch3lem  29418  dnnumch3  29419  fsuppeq  29469  pwfi2f1o  29470  diaintclN  34722  dibintclN  34831  dihintcl  35008