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

Theorem elpreima 6015
Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
elpreima  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  <->  ( B  e.  A  /\  ( F `  B )  e.  C ) ) )

Proof of Theorem elpreima
StepHypRef Expression
1 cnvimass 5205 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3461 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5691 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2493 . . . 4  |-  ( F  Fn  A  ->  ( B  e.  dom  F  <->  B  e.  A ) )
52, 4syl5ib 223 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  ->  B  e.  A )
)
6 fnfun 5689 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 6009 . . . . 5  |-  ( ( Fun  F  /\  B  e.  ( `' F " C ) )  -> 
( F `  B
)  e.  C )
86, 7sylan 474 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  ( `' F " C ) )  ->  ( F `  B )  e.  C
)
98ex 436 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( F `  B
)  e.  C ) )
105, 9jcad 536 . 2  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( B  e.  A  /\  ( F `  B
)  e.  C ) ) )
11 fvimacnv 6010 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5692 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1312biimpd 211 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  ->  B  e.  ( `' F " C ) ) )
1413expimpd 607 . 2  |-  ( F  Fn  A  ->  (
( B  e.  A  /\  ( F `  B
)  e.  C )  ->  B  e.  ( `' F " C ) ) )
1510, 14impbid 194 1  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  <->  ( B  e.  A  /\  ( F `  B )  e.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    e. wcel 1869   `'ccnv 4850   dom cdm 4851   "cima 4854   Fun wfun 5593    Fn wfn 5594   ` cfv 5599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-fv 5607
This theorem is referenced by:  fniniseg  6016  fncnvima2  6017  unpreima  6019  respreima  6022  fnse  6922  brwitnlem  7215  unxpwdom2  8107  smobeth  9013  fpwwe2lem6  9062  fpwwe2lem9  9065  hashkf  12518  isercolllem2  13722  isercolllem3  13723  isercoll  13724  fsumss  13784  fprodss  13995  tanval  14175  1arith  14864  0ram  14971  ghmpreima  16897  ghmnsgpreima  16900  torsubg  17485  kerf1hrm  17964  lmhmpreima  18264  evlslem3  18730  mpfind  18752  znunithash  19127  cncnpi  20286  cncnp  20288  cnpdis  20301  cnt0  20354  cnhaus  20362  2ndcomap  20465  1stccnp  20469  ptpjpre1  20578  tx1cn  20616  tx2cn  20617  txcnmpt  20631  txdis1cn  20642  hauseqlcld  20653  xkoptsub  20661  xkococn  20667  kqsat  20738  kqcldsat  20740  kqreglem1  20748  kqreglem2  20749  reghmph  20800  ordthmeolem  20808  tmdcn2  21096  clssubg  21115  tgphaus  21123  qustgplem  21127  ucncn  21292  xmeterval  21439  imasf1obl  21495  blval2  21569  metuel2  21572  isnghm  21720  isnghmOLD  21738  cnbl0  21786  cnblcld  21787  cnheiborlem  21974  nmhmcn  22126  ismbl  22472  mbfeqalem  22590  mbfmulc2lem  22595  mbfmax  22597  mbfposr  22600  mbfimaopnlem  22603  mbfaddlem  22608  mbfsup  22612  i1f1lem  22639  i1fpos  22656  mbfi1fseqlem4  22668  itg2monolem1  22700  itg2gt0  22710  itg2cnlem1  22711  itg2cnlem2  22712  plyeq0lem  23156  dgrlem  23175  dgrub  23180  dgrlb  23182  pserulm  23369  psercnlem2  23371  psercnlem1  23372  psercn  23373  abelth  23388  eff1olem  23489  ellogrn  23501  dvloglem  23585  logf1o2  23587  efopnlem1  23593  efopnlem2  23594  logtayl  23597  cxpcn3lem  23679  cxpcn3  23680  resqrtcn  23681  asinneg  23804  areambl  23876  sqff1o  24101  ubthlem1  26504  unipreima  28241  1stpreima  28283  2ndpreima  28284  suppss3  28312  kerunit  28588  smatrcl  28624  cnre2csqlem  28718  elzrhunit  28785  qqhval2lem  28787  qqhf  28792  1stmbfm  29084  2ndmbfm  29085  mbfmcnt  29092  eulerpartlemsv2  29193  eulerpartlemv  29199  eulerpartlemf  29205  eulerpartlemgvv  29211  eulerpartlemgh  29213  eulerpartlemgs2  29215  sseqmw  29226  sseqf  29227  sseqp1  29230  fiblem  29233  fibp1  29236  cvmseu  30001  cvmliftmolem1  30006  cvmliftmolem2  30007  cvmliftlem15  30023  cvmlift2lem10  30037  cvmlift3lem8  30051  elmthm  30216  mthmblem  30220  mclsppslem  30223  mclspps  30224  cnambfre  31947  dvtan  31950  ftc1anclem3  31977  ftc1anclem5  31979  areacirc  31995  sstotbnd2  32064  keridl  32223  ellkr  32618  pw2f1ocnv  35856  binomcxplemdvbinom  36604  binomcxplemcvg  36605  binomcxplemnotnn0  36607  rfcnpre1  37245  rfcnpre2  37257  rfcnpre3  37259  rfcnpre4  37260  icccncfext  37629  sge0fodjrnlem  38090
  Copyright terms: Public domain W3C validator