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

Theorem cnvimass 5033
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 5025 . 2  |-  ( `' A " B ) 
C_  ran  `' A
2 dfdm4 4872 . 2  |-  dom  A  =  ran  `' A
31, 2sseqtr4i 3211 1  |-  ( `' A " B ) 
C_  dom  A
Colors of variables: wff set class
Syntax hints:    C_ wss 3152   `'ccnv 4688   dom cdm 4689   ran crn 4690   "cima 4692
This theorem is referenced by:  fvimacnvi  5639  elpreima  5645  iinpreima  5655  fconst4  5736  pw2f1olem  6966  wemapso2  7267  cantnfcl  7368  cantnfle  7372  cantnflt  7373  cantnff  7375  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  cantnflem3  7393  cnfcomlem  7402  cnfcom  7403  cnfcom2lem  7404  cnfcom3lem  7406  cnfcom3  7407  infxpenlem  7641  enfin2i  7947  fin1a2lem7  8032  smobeth  8208  fpwwe2lem3  8255  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  canth4  8269  canthwelem  8272  pwfseqlem4  8284  recmulnq  8588  dmrecnq  8592  nn0supp  10017  ltweuz  11024  isercolllem2  12139  isercolllem3  12140  fsumss  12198  ackbijnn  12286  1arith  12974  vdwlem1  13028  vdwlem5  13032  vdwlem6  13033  vdwlem8  13035  vdwlem11  13038  fisuppfi  14450  ghmpreima  14704  gicer  14740  torsubg  15146  gsumval3  15191  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  gsumzoppg  15216  gsumunsn  15221  gsum2d  15223  dpjidcl  15293  lmhmpreima  15805  psrass1lem  16123  psrass1  16150  psrdi  16151  psrdir  16152  psrcom  16153  psrass23  16154  mplcoe1  16209  mplcoe2  16211  psr1baslem  16264  psropprmul  16316  coe1mul2  16346  gsumfsum  16439  cnpnei  16993  cnclima  16997  iscncl  16998  cnntri  17000  cnclsi  17001  cncls2  17002  cncls  17003  cnntr  17004  cncnp  17009  cnrest2  17014  cndis  17019  2ndcomap  17184  kgencn  17251  kgencn3  17253  ptbasfi  17276  txcnmpt  17318  txdis1cn  17329  qtopval2  17387  basqtop  17402  qtopcld  17404  qtopcn  17405  qtopeu  17407  qtoprest  17408  hmeoimaf1o  17461  hmphtop  17469  hmpher  17475  ordthmeolem  17492  elfm3  17645  rnelfmlem  17647  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  clssubg  17791  tgphaus  17799  divstgplem  17803  tsmsgsum  17821  xmeter  17979  imasf1oxms  18035  mbfconstlem  18984  i1fima  19033  i1fima2  19034  i1fd  19036  itg1addlem5  19055  mdegfval  19448  mdegleb  19450  mdegldg  19452  deg1mul3le  19502  plyeq0lem  19592  dgrcl  19615  dgrub  19616  dgrlb  19618  vieta1lem1  19690  vieta1lem2  19691  pserulm  19798  psercn2  19799  psercnlem2  19800  psercnlem1  19801  psercn  19802  pserdvlem1  19803  pserdvlem2  19804  pserdv  19805  pserdv2  19806  abelth  19817  eff1olem  19910  dvlog  19998  logtayl  20007  cxpcn3lem  20087  cxpcn3  20088  resqrcn  20089  wilthlem2  20307  wilthlem3  20308  basellem5  20322  elnlfn  22508  nlelshi  22640  xppreima  23211  indpreima  23608  indf1ofs  23609  cvmliftmolem1  23812  cvmlift2lem9  23842  cvmlift3lem6  23855  cvmlift3lem7  23856  intopcoaconlem3b  25538  intopcoaconlem3  25539  flfnei2  25577  islimrs4  25582  sstotbnd2  26498  keridl  26657  pw2f1ocnv  27130  dnnumch3lem  27143  dnnumch3  27144  frlmlbs  27249  fsuppeq  27259  pwfi2f1o  27260  diaintclN  31248  dibintclN  31357  dihintcl  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702
  Copyright terms: Public domain W3C validator