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

Theorem elpreima 5992
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 5348 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3493 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5671 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2530 . . . 4  |-  ( F  Fn  A  ->  ( B  e.  dom  F  <->  B  e.  A ) )
52, 4syl5ib 219 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  ->  B  e.  A )
)
6 fnfun 5669 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 5986 . . . . 5  |-  ( ( Fun  F  /\  B  e.  ( `' F " C ) )  -> 
( F `  B
)  e.  C )
86, 7sylan 471 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  ( `' F " C ) )  ->  ( F `  B )  e.  C
)
98ex 434 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( F `  B
)  e.  C ) )
105, 9jcad 533 . 2  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( B  e.  A  /\  ( F `  B
)  e.  C ) ) )
11 fvimacnv 5987 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5672 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1312biimpd 207 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  ->  B  e.  ( `' F " C ) ) )
1413expimpd 603 . 2  |-  ( F  Fn  A  ->  (
( B  e.  A  /\  ( F `  B
)  e.  C )  ->  B  e.  ( `' F " C ) ) )
1510, 14impbid 191 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 184    /\ wa 369    e. wcel 1762   `'ccnv 4991   dom cdm 4992   "cima 4995   Fun wfun 5573    Fn wfn 5574   ` cfv 5579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-fv 5587
This theorem is referenced by:  fniniseg  5993  fncnvima2  5994  rexsuppOLD  5997  unpreima  5998  respreima  6001  suppssOLD  6005  suppssrOLD  6006  fnse  6890  brwitnlem  7147  wemapso2OLD  7966  unxpwdom2  8003  cantnfleOLD  8109  cantnfp1lem2OLD  8113  cantnfp1lem3OLD  8114  cantnfp1OLD  8115  cantnflem1aOLD  8116  cantnflem1cOLD  8118  cantnflem3OLD  8121  mapfienOLD  8127  cnfcomlemOLD  8140  cnfcom3OLD  8145  smobeth  8950  fpwwe2lem6  9002  fpwwe2lem9  9005  hashkf  12362  isercolllem2  13437  isercolllem3  13438  isercoll  13439  fsumss  13496  tanval  13713  1arith  14293  0ram  14386  ghmpreima  16076  ghmnsgpreima  16079  torsubg  16646  kerf1hrm  17168  lmhmpreima  17470  evlslem3  17947  mpfind  17969  znunithash  18363  cncnpi  19538  cncnp  19540  cnpdis  19553  cnt0  19606  cnhaus  19614  2ndcomap  19718  1stccnp  19722  ptpjpre1  19800  tx1cn  19838  tx2cn  19839  txcnmpt  19853  txdis1cn  19864  hauseqlcld  19875  xkoptsub  19883  xkococn  19889  kqsat  19960  kqcldsat  19962  kqreglem1  19970  kqreglem2  19971  reghmph  20022  ordthmeolem  20030  tmdcn2  20316  clssubg  20335  tgphaus  20343  divstgplem  20347  ucncn  20516  xmeterval  20663  imasf1obl  20719  blval2  20806  metuel2  20810  isnghm  20958  cnbl0  21009  cnblcld  21010  cnheiborlem  21182  nmhmcn  21331  ismbl  21665  mbfeqalem  21777  mbfmulc2lem  21782  mbfmax  21784  mbfposr  21787  mbfimaopnlem  21790  mbfaddlem  21795  mbfsup  21799  i1f1lem  21824  i1fpos  21841  mbfi1fseqlem4  21853  itg2monolem1  21885  itg2gt0  21895  itg2cnlem1  21896  itg2cnlem2  21897  plyeq0lem  22335  dgrlem  22354  dgrub  22359  dgrlb  22361  pserulm  22544  psercnlem2  22546  psercnlem1  22547  psercn  22548  abelth  22563  eff1olem  22661  ellogrn  22668  dvloglem  22750  logf1o2  22752  efopnlem1  22758  efopnlem2  22759  logtayl  22762  cxpcn3lem  22842  cxpcn3  22843  resqrcn  22844  asinneg  22938  areambl  23009  sqff1o  23177  ubthlem1  25448  unipreima  27142  1stpreima  27182  2ndpreima  27183  suppss3  27208  kerunit  27462  cnre2csqlem  27514  elzrhunit  27582  qqhval2lem  27584  qqhf  27589  1stmbfm  27857  2ndmbfm  27858  mbfmcnt  27865  eulerpartlemsv2  27923  eulerpartlemv  27929  eulerpartlemf  27935  eulerpartlemgvv  27941  eulerpartlemgh  27943  eulerpartlemgs2  27945  sseqmw  27956  sseqf  27957  sseqp1  27960  fiblem  27963  fibp1  27966  cvmseu  28347  cvmliftmolem1  28352  cvmliftmolem2  28353  cvmliftlem15  28369  cvmlift2lem10  28383  cvmlift3lem8  28397  fprodss  28643  cnambfre  29627  dvtan  29629  ftc1anclem3  29656  ftc1anclem5  29658  areacirc  29676  sstotbnd2  29860  keridl  30019  pw2f1ocnv  30572  rfcnpre1  30927  rfcnpre2  30939  rfcnpre3  30941  rfcnpre4  30942  icccncfext  31181  ellkr  33761
  Copyright terms: Public domain W3C validator