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

Theorem fvelimab 5916
Description: Function value in an image. (Contributed by NM, 20-Jan-2007.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by David Abernethy, 17-Dec-2011.)
Assertion
Ref Expression
fvelimab  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( C  e.  ( F " B )  <->  E. x  e.  B  ( F `  x )  =  C ) )
Distinct variable groups:    x, B    x, C    x, F
Allowed substitution hint:    A( x)

Proof of Theorem fvelimab
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 elex 3117 . . 3  |-  ( C  e.  ( F " B )  ->  C  e.  _V )
21anim2i 569 . 2  |-  ( ( ( F  Fn  A  /\  B  C_  A )  /\  C  e.  ( F " B ) )  ->  ( ( F  Fn  A  /\  B  C_  A )  /\  C  e.  _V )
)
3 fvex 5869 . . . . 5  |-  ( F `
 x )  e. 
_V
4 eleq1 2534 . . . . 5  |-  ( ( F `  x )  =  C  ->  (
( F `  x
)  e.  _V  <->  C  e.  _V ) )
53, 4mpbii 211 . . . 4  |-  ( ( F `  x )  =  C  ->  C  e.  _V )
65rexlimivw 2947 . . 3  |-  ( E. x  e.  B  ( F `  x )  =  C  ->  C  e.  _V )
76anim2i 569 . 2  |-  ( ( ( F  Fn  A  /\  B  C_  A )  /\  E. x  e.  B  ( F `  x )  =  C )  ->  ( ( F  Fn  A  /\  B  C_  A )  /\  C  e.  _V )
)
8 eleq1 2534 . . . . . 6  |-  ( y  =  C  ->  (
y  e.  ( F
" B )  <->  C  e.  ( F " B ) ) )
9 eqeq2 2477 . . . . . . 7  |-  ( y  =  C  ->  (
( F `  x
)  =  y  <->  ( F `  x )  =  C ) )
109rexbidv 2968 . . . . . 6  |-  ( y  =  C  ->  ( E. x  e.  B  ( F `  x )  =  y  <->  E. x  e.  B  ( F `  x )  =  C ) )
118, 10bibi12d 321 . . . . 5  |-  ( y  =  C  ->  (
( y  e.  ( F " B )  <->  E. x  e.  B  ( F `  x )  =  y )  <->  ( C  e.  ( F " B
)  <->  E. x  e.  B  ( F `  x )  =  C ) ) )
1211imbi2d 316 . . . 4  |-  ( y  =  C  ->  (
( ( F  Fn  A  /\  B  C_  A
)  ->  ( y  e.  ( F " B
)  <->  E. x  e.  B  ( F `  x )  =  y ) )  <-> 
( ( F  Fn  A  /\  B  C_  A
)  ->  ( C  e.  ( F " B
)  <->  E. x  e.  B  ( F `  x )  =  C ) ) ) )
13 fnfun 5671 . . . . . . 7  |-  ( F  Fn  A  ->  Fun  F )
1413adantr 465 . . . . . 6  |-  ( ( F  Fn  A  /\  B  C_  A )  ->  Fun  F )
15 fndm 5673 . . . . . . . 8  |-  ( F  Fn  A  ->  dom  F  =  A )
1615sseq2d 3527 . . . . . . 7  |-  ( F  Fn  A  ->  ( B  C_  dom  F  <->  B  C_  A
) )
1716biimpar 485 . . . . . 6  |-  ( ( F  Fn  A  /\  B  C_  A )  ->  B  C_  dom  F )
18 dfimafn 5909 . . . . . 6  |-  ( ( Fun  F  /\  B  C_ 
dom  F )  -> 
( F " B
)  =  { y  |  E. x  e.  B  ( F `  x )  =  y } )
1914, 17, 18syl2anc 661 . . . . 5  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( F " B
)  =  { y  |  E. x  e.  B  ( F `  x )  =  y } )
2019abeq2d 2588 . . . 4  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( y  e.  ( F " B )  <->  E. x  e.  B  ( F `  x )  =  y ) )
2112, 20vtoclg 3166 . . 3  |-  ( C  e.  _V  ->  (
( F  Fn  A  /\  B  C_  A )  ->  ( C  e.  ( F " B
)  <->  E. x  e.  B  ( F `  x )  =  C ) ) )
2221impcom 430 . 2  |-  ( ( ( F  Fn  A  /\  B  C_  A )  /\  C  e.  _V )  ->  ( C  e.  ( F " B
)  <->  E. x  e.  B  ( F `  x )  =  C ) )
232, 7, 22pm5.21nd 895 1  |-  ( ( F  Fn  A  /\  B  C_  A )  -> 
( C  e.  ( F " B )  <->  E. x  e.  B  ( F `  x )  =  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1374    e. wcel 1762   {cab 2447   E.wrex 2810   _Vcvv 3108    C_ wss 3471   dom cdm 4994   "cima 4997   Fun wfun 5575    Fn wfn 5576   ` cfv 5581
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 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681
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 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-opab 4501  df-id 4790  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-fv 5589
This theorem is referenced by:  ssimaex  5925  rexima  6132  ralima  6133  f1elima  6152  ovelimab  6430  tcrank  8293  ackbij2  8614  fin1a2lem6  8776  iunfo  8905  grothomex  9198  axpre-sup  9537  injresinjlem  11884  lmhmima  17471  txkgen  19883  fmucndlem  20524  mdegldg  22196  ig1peu  22302  efopn  22762  cusgrares  24136  pjimai  26759  fimaproj  27487  qtophaus  27625  indf1ofs  27667  eulerpartgbij  27939  eulerpartlemgvv  27943  ballotlemsima  28082  nocvxmin  29016  isnacs2  30231  isnacs3  30235  islmodfg  30610  kercvrlsm  30624  isnumbasgrplem2  30648  dfacbasgrp  30652  unima  30976  fourierdlem62  31426
  Copyright terms: Public domain W3C validator