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

Theorem elpreima 5645
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 5033 . . . . 5  |-  ( `' F " C ) 
C_  dom  F
21sseli 3176 . . . 4  |-  ( B  e.  ( `' F " C )  ->  B  e.  dom  F )
3 fndm 5343 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
43eleq2d 2350 . . . 4  |-  ( F  Fn  A  ->  ( B  e.  dom  F  <->  B  e.  A ) )
52, 4syl5ib 210 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  ->  B  e.  A )
)
6 fnfun 5341 . . . . 5  |-  ( F  Fn  A  ->  Fun  F )
7 fvimacnvi 5639 . . . . 5  |-  ( ( Fun  F  /\  B  e.  ( `' F " C ) )  -> 
( F `  B
)  e.  C )
86, 7sylan 457 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  ( `' F " C ) )  ->  ( F `  B )  e.  C
)
98ex 423 . . 3  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( F `  B
)  e.  C ) )
105, 9jcad 519 . 2  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  -> 
( B  e.  A  /\  ( F `  B
)  e.  C ) ) )
11 fvimacnv 5640 . . . . 5  |-  ( ( Fun  F  /\  B  e.  dom  F )  -> 
( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1211funfni 5344 . . . 4  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  <->  B  e.  ( `' F " C ) ) )
1312biimpd 198 . . 3  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( ( F `  B )  e.  C  ->  B  e.  ( `' F " C ) ) )
1413expimpd 586 . 2  |-  ( F  Fn  A  ->  (
( B  e.  A  /\  ( F `  B
)  e.  C )  ->  B  e.  ( `' F " C ) ) )
1510, 14impbid 183 1  |-  ( F  Fn  A  ->  ( B  e.  ( `' F " C )  <->  ( B  e.  A  /\  ( F `  B )  e.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1684   `'ccnv 4688   dom cdm 4689   "cima 4692   Fun wfun 5249    Fn wfn 5250   ` cfv 5255
This theorem is referenced by:  fniniseg  5646  fncnvima2  5647  rexsupp  5650  unpreima  5651  respreima  5654  suppss  5658  suppssr  5659  fnse  6232  brwitnlem  6506  wemapso2  7267  unxpwdom2  7302  cantnfle  7372  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnfp1  7383  oemapvali  7386  cantnflem1a  7387  cantnflem1c  7389  cantnflem3  7393  mapfien  7399  cnfcomlem  7402  cnfcom3  7407  smobeth  8208  fpwwe2lem6  8257  fpwwe2lem9  8260  hashkf  11339  isercolllem2  12139  isercolllem3  12140  isercoll  12141  fsumss  12198  tanval  12408  1arith  12974  0ram  13067  ghmpreima  14704  ghmnsgpreima  14707  torsubg  15146  lmhmpreima  15805  znunithash  16518  cncnpi  17007  cncnp  17009  cnpdis  17021  cnt0  17074  cnhaus  17082  2ndcomap  17184  1stccnp  17188  ptpjpre1  17266  tx1cn  17303  tx2cn  17304  txcnmpt  17318  txdis1cn  17329  hauseqlcld  17340  xkoptsub  17348  xkococn  17354  kqsat  17422  kqcldsat  17424  kqreglem1  17432  kqreglem2  17433  reghmph  17484  ordthmeolem  17492  tmdcn2  17772  clssubg  17791  tgphaus  17799  divstgplem  17803  xmeterval  17978  imasf1obl  18034  isnghm  18232  cnbl0  18283  cnblcld  18284  cnheiborlem  18452  nmhmcn  18601  ismbl  18885  mbfeqalem  18997  mbfmulc2lem  19002  mbfmax  19004  mbfposr  19007  mbfimaopnlem  19010  mbfaddlem  19015  mbfsup  19019  i1f1lem  19044  i1fpos  19061  mbfi1fseqlem4  19073  itg2monolem1  19105  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  evlslem3  19398  mpfind  19428  mdegleb  19450  plyeq0lem  19592  dgrlem  19611  dgrub  19616  dgrlb  19618  pserulm  19798  psercnlem2  19800  psercnlem1  19801  psercn  19802  abelth  19817  eff1olem  19910  ellogrn  19917  dvloglem  19995  logf1o2  19997  efopnlem1  20003  efopnlem2  20004  logtayl  20007  cxpcn3lem  20087  cxpcn3  20088  resqrcn  20089  asinneg  20182  areambl  20253  sqff1o  20420  ubthlem1  21449  unipreima  23209  cnre2csqlem  23294  1stmbfm  23565  2ndmbfm  23566  mbfmcnt  23573  cvmseu  23807  cvmliftmolem1  23812  cvmliftmolem2  23813  cvmliftlem15  23829  cvmlift2lem10  23843  cvmlift3lem8  23857  areacirc  24931  sstotbnd2  26498  keridl  26657  pw2f1ocnv  27130  rfcnpre1  27690  rfcnpre2  27702  rfcnpre3  27704  rfcnpre4  27705  ellkr  29279
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-sbc 2992  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-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-fv 5263
  Copyright terms: Public domain W3C validator