Theorem fvelima 5915

Description: Function value in an image. Part of Theorem 4.4(iii) of [Monk1] p. 42. (Contributed by NM, 29-Apr-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
fvelima	|- ( ( Fun F /\ A e. ( F " B ) ) -> E. x e. B ( F ` x ) = A )

Distinct variable groups:   x, A   x, B   x, F

Proof of Theorem fvelima

Step	Hyp	Ref	Expression
1		elimag 5171	. . . 4 |- ( A e. ( F " B ) -> ( A e. ( F " B ) <-> E. x e. B x F A ) )
2	1	ibi 245	. . 3 |- ( A e. ( F " B ) -> E. x e. B x F A )
3		funbrfv 5901	. . . 4 |- ( Fun F -> ( x F A -> ( F ` x ) = A ) )
4	3	reximdv 2860	. . 3 |- ( Fun F -> ( E. x e. B x F A -> E. x e. B ( F ` x ) = A ) )
5	2, 4	syl5 33	. 2 |- ( Fun F -> ( A e. ( F " B ) -> E. x e. B ( F ` x ) = A ) )
6	5	imp 431	1 |- ( ( Fun F /\ A e. ( F " B ) ) -> E. x e. B ( F ` x ) = A )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1443   e. wcel 1886   E.wrex 2737   class class class wbr 4401   "cima 4836   Fun wfun 5575   ` cfv 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fv 5589

This theorem is referenced by:  ssimaex  5928  isofrlem  6229  tz7.49  7159  rankwflemb  8261  tcrank  8352  zorn2lem5  8927  zorn2lem6  8928  uniimadom  8966  wunr1om  9141  tskr1om  9189  tskr1om2  9190  grur1  9242  iscldtop  20104  kqfvima  20738  fmfnfmlem4  20965  fmfnfm  20966  qustgpopn  21127  c1liplem1  22941  plypf1  23159  ltgseg  24634  axcontlem9  24995  htthlem  26563  xrofsup  28346  fimaproj  28653  txomap  28654  qtophaus  28656  erdszelem7  29913  erdszelem8  29914  mrsub0  30147  mrsubccat  30149  mrsubcn  30150  msubrn  30160  mthmblem  30211  ivthALT  30984  ftc2nc  32019  heibor1lem  32134  ismrc  35537  icccncfext  37759  dirkercncflem2  37960  uhgrspan1  39358