Theorem fvelima 6899

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 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹

Proof of Theorem fvelima

Step	Hyp	Ref	Expression
1		funbrfv 6882	. . 3 ⊢ (Fun 𝐹 → (𝑥𝐹𝐴 → (𝐹‘𝑥) = 𝐴))
2	1	reximdv 3155	. 2 ⊢ (Fun 𝐹 → (∃𝑥 ∈ 𝐵 𝑥𝐹𝐴 → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴))
3		elimag 6023	. . 3 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → (𝐴 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴))
4	3	ibi 268	. 2 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴)
5	2, 4	impel 510	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃wrex 3064   class class class wbr 5079   “ cima 5628  Fun wfun 6486  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  funimassd  6900  ssimaex  6919  isofrlem  7291  fimaproj  8082  tz7.49  8381  rankwflemb  9715  tcrank  9806  zorn2lem5  10420  zorn2lem6  10421  uniimadom  10464  wunr1om  10640  tskr1om  10688  tskr1om2  10689  grur1  10741  imadrhmcl  20776  iscldtop  23085  kqfvima  23720  fmfnfmlem4  23947  fmfnfm  23948  qustgpopn  24110  cphsscph  25243  c1liplem1  25988  plypf1  26202  lrrecfr  27960  ltgseg  28689  axcontlem9  29066  uhgrspan1  29397  pthdlem2lem  29860  htthlem  31013  xrofsup  32866  tocyccntz  33232  rhmimaidl  33522  esplymhp  33759  dimval  33792  dimvalfi  33793  txomap  34025  qtophaus  34027  erdszelem7  35432  erdszelem8  35433  mrsub0  35751  mrsubccat  35753  mrsubcn  35754  msubrn  35764  mthmblem  35815  ivthALT  36570  weiunfr  36702  ftc2nc  38076  heibor1lem  38183  aks6d1c4  42616  imacrhmcl  43011  ismrc  43157  relpfrlem  45404  icccncfext  46337  dirkercncflem2  46554  smfpimbor1lem1  47248  imaf1co  49652