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

Theorem elpreima 6017
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 5194 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3414 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5685 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2534 . . . 4  |-  ( F  Fn  A  ->  ( B  e.  dom  F  <->  B  e.  A ) )
52, 4syl5ib 227 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  ->  B  e.  A )
)
6 fnfun 5683 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 6011 . . . . 5  |-  ( ( Fun  F  /\  B  e.  ( `' F " C ) )  -> 
( F `  B
)  e.  C )
86, 7sylan 479 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  ( `' F " C ) )  ->  ( F `  B )  e.  C
)
98ex 441 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( F `  B
)  e.  C ) )
105, 9jcad 542 . 2  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( B  e.  A  /\  ( F `  B
)  e.  C ) ) )
11 fvimacnv 6012 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5686 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1312biimpd 212 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  ->  B  e.  ( `' F " C ) ) )
1413expimpd 614 . 2  |-  ( F  Fn  A  ->  (
( B  e.  A  /\  ( F `  B
)  e.  C )  ->  B  e.  ( `' F " C ) ) )
1510, 14impbid 195 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 189    /\ wa 376    e. wcel 1904   `'ccnv 4838   dom cdm 4839   "cima 4842   Fun wfun 5583    Fn wfn 5584   ` cfv 5589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-fv 5597
This theorem is referenced by:  fniniseg  6018  fncnvima2  6019  unpreima  6021  respreima  6024  fnse  6932  brwitnlem  7227  unxpwdom2  8121  smobeth  9029  fpwwe2lem6  9078  fpwwe2lem9  9081  hashkf  12555  isercolllem2  13806  isercolllem3  13807  isercoll  13808  fsumss  13868  fprodss  14079  tanval  14259  1arith  14950  0ram  15057  ghmpreima  16982  ghmnsgpreima  16985  torsubg  17570  kerf1hrm  18049  lmhmpreima  18349  evlslem3  18814  mpfind  18836  znunithash  19212  cncnpi  20371  cncnp  20373  cnpdis  20386  cnt0  20439  cnhaus  20447  2ndcomap  20550  1stccnp  20554  ptpjpre1  20663  tx1cn  20701  tx2cn  20702  txcnmpt  20716  txdis1cn  20727  hauseqlcld  20738  xkoptsub  20746  xkococn  20752  kqsat  20823  kqcldsat  20825  kqreglem1  20833  kqreglem2  20834  reghmph  20885  ordthmeolem  20893  tmdcn2  21182  clssubg  21201  tgphaus  21209  qustgplem  21213  ucncn  21378  xmeterval  21525  imasf1obl  21581  blval2  21655  metuel2  21658  isnghm  21806  isnghmOLD  21824  cnbl0  21872  cnblcld  21873  cnheiborlem  22060  nmhmcn  22212  ismbl  22558  mbfeqalem  22677  mbfmulc2lem  22682  mbfmax  22684  mbfposr  22687  mbfimaopnlem  22690  mbfaddlem  22695  mbfsup  22699  i1f1lem  22726  i1fpos  22743  mbfi1fseqlem4  22755  itg2monolem1  22787  itg2gt0  22797  itg2cnlem1  22798  itg2cnlem2  22799  plyeq0lem  23243  dgrlem  23262  dgrub  23267  dgrlb  23269  pserulm  23456  psercnlem2  23458  psercnlem1  23459  psercn  23460  abelth  23475  eff1olem  23576  ellogrn  23588  dvloglem  23672  logf1o2  23674  efopnlem1  23680  efopnlem2  23681  logtayl  23684  cxpcn3lem  23766  cxpcn3  23767  resqrtcn  23768  asinneg  23891  areambl  23963  sqff1o  24188  ubthlem1  26593  unipreima  28321  1stpreima  28362  2ndpreima  28363  suppss3  28387  kerunit  28660  smatrcl  28696  cnre2csqlem  28790  elzrhunit  28857  qqhval2lem  28859  qqhf  28864  1stmbfm  29155  2ndmbfm  29156  mbfmcnt  29163  eulerpartlemsv2  29264  eulerpartlemv  29270  eulerpartlemf  29276  eulerpartlemgvv  29282  eulerpartlemgh  29284  eulerpartlemgs2  29286  sseqmw  29297  sseqf  29298  sseqp1  29301  fiblem  29304  fibp1  29307  cvmseu  30071  cvmliftmolem1  30076  cvmliftmolem2  30077  cvmliftlem15  30093  cvmlift2lem10  30107  cvmlift3lem8  30121  elmthm  30286  mthmblem  30290  mclsppslem  30293  mclspps  30294  cnambfre  32053  dvtan  32056  ftc1anclem3  32083  ftc1anclem5  32085  areacirc  32101  sstotbnd2  32170  keridl  32329  ellkr  32726  pw2f1ocnv  35963  binomcxplemdvbinom  36772  binomcxplemcvg  36773  binomcxplemnotnn0  36775  rfcnpre1  37403  rfcnpre2  37415  rfcnpre3  37417  rfcnpre4  37418  icccncfext  37862  sge0fodjrnlem  38372
  Copyright terms: Public domain W3C validator