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

Theorem elpreima 6007
Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
elpreima

Proof of Theorem elpreima
StepHypRef Expression
1 cnvimass 5362 . . . . 5
21sseli 3499 . . . 4
3 fndm 5685 . . . . 5
43eleq2d 2527 . . . 4
52, 4syl5ib 219 . . 3
6 fnfun 5683 . . . . 5
7 fvimacnvi 6001 . . . . 5
86, 7sylan 471 . . . 4
98ex 434 . . 3
105, 9jcad 533 . 2
11 fvimacnv 6002 . . . . 5
1211funfni 5686 . . . 4
1312biimpd 207 . . 3
1413expimpd 603 . 2
1510, 14impbid 191 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818  `'ccnv 5003  domcdm 5004  "cima 5007  Funwfun 5587  Fnwfn 5588  `cfv 5593
This theorem is referenced by:  fniniseg  6008  fncnvima2  6009  rexsuppOLD  6012  unpreima  6013  respreima  6016  suppssOLD  6020  suppssrOLD  6021  fnse  6917  brwitnlem  7176  wemapso2OLD  7998  unxpwdom2  8035  cantnfleOLD  8141  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  cantnflem1aOLD  8148  cantnflem1cOLD  8150  cantnflem3OLD  8153  mapfienOLD  8159  cnfcomlemOLD  8172  cnfcom3OLD  8177  smobeth  8982  fpwwe2lem6  9034  fpwwe2lem9  9037  hashkf  12407  isercolllem2  13488  isercolllem3  13489  isercoll  13490  fsumss  13547  fprodss  13755  tanval  13863  1arith  14445  0ram  14538  ghmpreima  16288  ghmnsgpreima  16291  torsubg  16860  kerf1hrm  17392  lmhmpreima  17694  evlslem3  18183  mpfind  18205  znunithash  18603  cncnpi  19779  cncnp  19781  cnpdis  19794  cnt0  19847  cnhaus  19855  2ndcomap  19959  1stccnp  19963  ptpjpre1  20072  tx1cn  20110  tx2cn  20111  txcnmpt  20125  txdis1cn  20136  hauseqlcld  20147  xkoptsub  20155  xkococn  20161  kqsat  20232  kqcldsat  20234  kqreglem1  20242  kqreglem2  20243  reghmph  20294  ordthmeolem  20302  tmdcn2  20588  clssubg  20607  tgphaus  20615  qustgplem  20619  ucncn  20788  xmeterval  20935  imasf1obl  20991  blval2  21078  metuel2  21082  isnghm  21230  cnbl0  21281  cnblcld  21282  cnheiborlem  21454  nmhmcn  21603  ismbl  21937  mbfeqalem  22049  mbfmulc2lem  22054  mbfmax  22056  mbfposr  22059  mbfimaopnlem  22062  mbfaddlem  22067  mbfsup  22071  i1f1lem  22096  i1fpos  22113  mbfi1fseqlem4  22125  itg2monolem1  22157  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  plyeq0lem  22607  dgrlem  22626  dgrub  22631  dgrlb  22633  pserulm  22817  psercnlem2  22819  psercnlem1  22820  psercn  22821  abelth  22836  eff1olem  22935  ellogrn  22947  dvloglem  23029  logf1o2  23031  efopnlem1  23037  efopnlem2  23038  logtayl  23041  cxpcn3lem  23121  cxpcn3  23122  resqrtcn  23123  asinneg  23217  areambl  23288  sqff1o  23456  ubthlem1  25786  unipreima  27484  1stpreima  27524  2ndpreima  27525  suppss3  27550  kerunit  27813  cnre2csqlem  27892  elzrhunit  27960  qqhval2lem  27962  qqhf  27967  1stmbfm  28231  2ndmbfm  28232  mbfmcnt  28239  eulerpartlemsv2  28297  eulerpartlemv  28303  eulerpartlemf  28309  eulerpartlemgvv  28315  eulerpartlemgh  28317  eulerpartlemgs2  28319  sseqmw  28330  sseqf  28331  sseqp1  28334  fiblem  28337  fibp1  28340  cvmseu  28721  cvmliftmolem1  28726  cvmliftmolem2  28727  cvmliftlem15  28743  cvmlift2lem10  28757  cvmlift3lem8  28771  elmthm  28936  mthmblem  28940  mclsppslem  28943  mclspps  28944  cnambfre  30063  dvtan  30065  ftc1anclem3  30092  ftc1anclem5  30094  areacirc  30112  sstotbnd2  30270  keridl  30429  pw2f1ocnv  30979  binomcxplemdvbinom  31258  binomcxplemcvg  31259  binomcxplemnotnn0  31261  rfcnpre1  31394  rfcnpre2  31406  rfcnpre3  31408  rfcnpre4  31409  icccncfext  31690  ellkr  34814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-fv 5601
  Copyright terms: Public domain W3C validator