Theorem fvelima 6976

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 6959	. . 3 ⊢ (Fun 𝐹 → (𝑥𝐹𝐴 → (𝐹‘𝑥) = 𝐴))
2	1	reximdv 3181	. 2 ⊢ (Fun 𝐹 → (∃𝑥 ∈ 𝐵 𝑥𝐹𝐴 → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴))
3		elimag 6073	. . 3 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → (𝐴 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴))
4	3	ibi 270	. 2 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴)
5	2, 4	impel 515	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃wrex 3090   class class class wbr 5106   “ cima 5659  Fun wfun 6555  ‘cfv 6561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fv 6569

This theorem is used by:  funimassd  6977  ssimaex  6996  isofrlem  7374  fimaproj  8182  tz7.49  8486  rankwflemb  9830  rankwflembOLD  9831  tcrank  9931  zorn2lem5  10608  zorn2lem6  10609  uniimadom  10658  wunr1om  10834  tskr1om  10882  tskhf  10883  grur1  10935  imadrhmcl  21087  iscldtop  23446  kqfvima  24082  fmfnfmlem4  24309  fmfnfm  24310  qustgpopn  24472  cphsscph  25605  c1liplem1  26349  plypf1  26564  lrrecfr  28362  ltgseg  29092  axcontlem9  29583  uhgrspan1  29917  pthdlem2lem  30386  htthlem  31552  xrofsup  33432  tocyccntz  33781  rhmimaidl  34066  esplymhp  34283  dimval  34316  dimvalfi  34317  txomap  34549  qtophaus  34551  acwer1prc  35865  erdszelem7  36142  erdszelem8  36143  mrsub0  36461  mrsubccat  36463  mrsubcn  36464  msubrn  36474  mthmblem  36525  ivthALT  37314  weiunfr  37446  ftc2nc  38825  heibor1lem  38946  aks6d1c4  43377  imacrhmcl  43785  ismrc  43916  relpfrlem  46149  icccncfext  47112  dirkercncflem2  47329  smfpimbor1lem1  48023  imaf1co  50486