MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvimass Unicode version

Theorem cnvimass 5049
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
StepHypRef Expression
1 imassrn 5041 . 2  |-  ( `' A " B ) 
C_  ran  `' A
2 dfdm4 4888 . 2  |-  dom  A  =  ran  `' A
31, 2sseqtr4i 3224 1  |-  ( `' A " B ) 
C_  dom  A
Colors of variables: wff set class
Syntax hints:    C_ wss 3165   `'ccnv 4704   dom cdm 4705   ran crn 4706   "cima 4708
This theorem is referenced by:  fvimacnvi  5655  elpreima  5661  iinpreima  5671  fconst4  5752  pw2f1olem  6982  wemapso2  7283  cantnfcl  7384  cantnfle  7388  cantnflt  7389  cantnff  7391  cantnfp1lem2  7397  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1d  7406  cantnflem1  7407  cantnflem3  7409  cnfcomlem  7418  cnfcom  7419  cnfcom2lem  7420  cnfcom3lem  7422  cnfcom3  7423  infxpenlem  7657  enfin2i  7963  fin1a2lem7  8048  smobeth  8224  fpwwe2lem3  8271  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  canth4  8285  canthwelem  8288  pwfseqlem4  8300  recmulnq  8604  dmrecnq  8608  nn0supp  10033  ltweuz  11040  isercolllem2  12155  isercolllem3  12156  fsumss  12214  ackbijnn  12302  1arith  12990  vdwlem1  13044  vdwlem5  13048  vdwlem6  13049  vdwlem8  13051  vdwlem11  13054  fisuppfi  14466  ghmpreima  14720  gicer  14756  torsubg  15162  gsumval3  15207  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumconst  15225  gsumzmhm  15226  gsumzoppg  15232  gsumunsn  15237  gsum2d  15239  dpjidcl  15309  lmhmpreima  15821  psrass1lem  16139  psrass1  16166  psrdi  16167  psrdir  16168  psrcom  16169  psrass23  16170  mplcoe1  16225  mplcoe2  16227  psr1baslem  16280  psropprmul  16332  coe1mul2  16362  gsumfsum  16455  cnpnei  17009  cnclima  17013  iscncl  17014  cnntri  17016  cnclsi  17017  cncls2  17018  cncls  17019  cnntr  17020  cncnp  17025  cnrest2  17030  cndis  17035  2ndcomap  17200  kgencn  17267  kgencn3  17269  ptbasfi  17292  txcnmpt  17334  txdis1cn  17345  qtopval2  17403  basqtop  17418  qtopcld  17420  qtopcn  17421  qtopeu  17423  qtoprest  17424  hmeoimaf1o  17477  hmphtop  17485  hmpher  17491  ordthmeolem  17508  elfm3  17661  rnelfmlem  17663  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  clssubg  17807  tgphaus  17815  divstgplem  17819  tsmsgsum  17837  xmeter  17995  imasf1oxms  18051  mbfconstlem  19000  i1fima  19049  i1fima2  19050  i1fd  19052  itg1addlem5  19071  mdegfval  19464  mdegleb  19466  mdegldg  19468  deg1mul3le  19518  plyeq0lem  19608  dgrcl  19631  dgrub  19632  dgrlb  19634  vieta1lem1  19706  vieta1lem2  19707  pserulm  19814  psercn2  19815  psercnlem2  19816  psercnlem1  19817  psercn  19818  pserdvlem1  19819  pserdvlem2  19820  pserdv  19821  pserdv2  19822  abelth  19833  eff1olem  19926  dvlog  20014  logtayl  20023  cxpcn3lem  20103  cxpcn3  20104  resqrcn  20105  wilthlem2  20323  wilthlem3  20324  basellem5  20338  elnlfn  22524  nlelshi  22656  xppreima  23226  indpreima  23623  indf1ofs  23624  cvmliftmolem1  23827  cvmlift2lem9  23857  cvmlift3lem6  23870  cvmlift3lem7  23871  itg2addnclem  25003  intopcoaconlem3b  25641  intopcoaconlem3  25642  flfnei2  25680  islimrs4  25685  sstotbnd2  26601  keridl  26760  pw2f1ocnv  27233  dnnumch3lem  27246  dnnumch3  27247  frlmlbs  27352  fsuppeq  27362  pwfi2f1o  27363  diaintclN  31870  dibintclN  31979  dihintcl  32156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-opab 4094  df-xp 4711  df-cnv 4713  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718
  Copyright terms: Public domain W3C validator