Theorem cnvimass 5186

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

Syntax hints:   C_ wss 3325   `'ccnv 4835   dom cdm 4836   ran crn 4837   "cima 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-xp 4842  df-cnv 4844  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849

This theorem is referenced by:  fvimacnvi  5814  elpreima  5820  iinpreima  5830  fconst4  5939  frnsuppeq  6701  pw2f1olem  7411  cnvimamptfin  7608  fisuppfi  7624  wemapso2OLD  7762  cantnfclOLD  7901  cantnfleOLD  7905  cantnfltOLD  7906  cantnfp1lem2OLD  7909  cantnfp1lem3OLD  7910  cantnflem1bOLD  7913  cantnflem1dOLD  7915  cantnflem1OLD  7916  cantnflem3OLD  7917  cnfcomlemOLD  7936  cnfcomOLD  7937  cnfcom2lemOLD  7938  cnfcom3lemOLD  7940  cnfcom3OLD  7941  infxpenlem  8176  enfin2i  8486  fin1a2lem7  8571  smobeth  8746  fpwwe2lem3  8796  fpwwe2lem12  8804  fpwwe2lem13  8805  fpwwe2  8806  canth4  8810  canthwelem  8813  pwfseqlem4  8825  recmulnq  9129  dmrecnq  9133  nn0suppOLD  10630  ltweuz  11780  isercolllem2  13139  isercolllem3  13140  fsumss  13198  ackbijnn  13287  1arith  13984  vdwlem1  14038  vdwlem5  14042  vdwlem6  14043  vdwlem8  14045  vdwlem11  14048  ghmpreima  15761  gicer  15797  torsubg  16329  gsumval3OLD  16375  gsumzresOLD  16385  gsumzclOLD  16386  gsumzf1oOLD  16387  gsumzaddlemOLD  16403  gsumzmhm  16422  gsumzmhmOLD  16423  gsumzoppg  16432  gsumzoppgOLD  16433  gsum2dOLD  16454  dpjidclOLD  16554  lmhmpreima  17107  mplcoe2  17525  mplcoe2OLD  17526  psr1baslem  17617  evpmss  17975  ofco2  18291  cnpnei  18827  cnclima  18831  iscncl  18832  cnntri  18834  cnclsi  18835  cncls2  18836  cncls  18837  cnntr  18838  cncnp  18843  cnrest2  18849  cndis  18854  2ndcomap  19021  kgencn  19088  kgencn3  19090  ptbasfi  19113  txcnmpt  19156  txdis1cn  19167  qtopval2  19228  basqtop  19243  qtopcld  19245  qtopcn  19246  qtopeu  19248  qtoprest  19249  hmeoimaf1o  19302  hmphtop  19310  hmpher  19316  ordthmeolem  19333  elfm3  19482  rnelfmlem  19484  rnelfm  19485  fmfnfmlem2  19487  fmfnfmlem4  19489  clssubg  19638  tgphaus  19646  divstgplem  19650  tsmsgsumOLD  19671  ucnprima  19816  ucncn  19819  xmeter  19967  imasf1oxms  20023  metustssOLD  20087  metustss  20088  metustexhalfOLD  20097  metustexhalf  20098  metustfbasOLD  20099  metustfbas  20100  cfilucfilOLD  20103  cfilucfil  20104  metuel2  20113  restmetu  20121  mbfconstlem  21066  i1fima  21115  i1fima2  21116  i1fd  21118  itg1addlem5  21137  plyeq0lem  21637  dgrcl  21660  dgrub  21661  dgrlb  21663  vieta1lem1  21735  vieta1lem2  21736  pserulm  21846  psercn2  21847  psercnlem2  21848  psercnlem1  21849  psercn  21850  pserdvlem1  21851  pserdvlem2  21852  pserdv  21853  pserdv2  21854  abelth  21865  eff1olem  21963  dvlog  22055  logtayl  22064  cxpcn3lem  22144  cxpcn3  22145  resqrcn  22146  basellem5  22381  elnlfn  25267  nlelshi  25399  xppreima  25899  ofpreima  25919  ofpreima2  25920  ffsrn  25964  gsumunsnf  26180  gsumle  26181  indpreima  26417  indf1ofs  26418  sibfof  26656  sitgclg  26658  eulerpartlemsv2  26671  eulerpartlemsf  26672  eulerpartlemv  26677  eulerpartlemb  26681  eulerpartlemt  26684  eulerpartlemr  26687  eulerpartlemgu  26690  eulerpartlemgs2  26693  eulerpartlemn  26694  cvmliftmolem1  27100  cvmlift2lem9  27130  cvmlift3lem6  27143  cvmlift3lem7  27144  fprodss  27390  dvtan  28367  itg2addnclem  28368  ftc1anclem6  28397  sstotbnd2  28598  keridl  28757  pw2f1ocnv  29311  dnnumch3lem  29324  dnnumch3  29325  fsuppeq  29375  pwfi2f1o  29376  diaintclN  34425  dibintclN  34534  dihintcl  34711