Theorem fvelima 6949

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∃wrex 3095   class class class wbr 5113   “ cima 5667  Fun wfun 6533  ‘cfv 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5407

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-iota 6495  df-fun 6541  df-fv 6547

This theorem is referenced by:  funimassd  6950  ssimaex  6969  isofrlem  7341  fimaproj  8133  tz7.49  8434  rankwflemb  9767  tcrank  9858  zorn2lem5  10486  zorn2lem6  10487  uniimadom  10530  wunr1om  10706  tskr1om  10754  tskr1om2  10755  grur1  10807  imadrhmcl  20880  iscldtop  23223  kqfvima  23858  fmfnfmlem4  24085  fmfnfm  24086  qustgpopn  24248  cphsscph  25381  c1liplem1  26126  plypf1  26340  lrrecfr  28104  ltgseg  28833  axcontlem9  29265  uhgrspan1  29596  pthdlem2lem  30059  htthlem  31212  xrofsup  33055  tocyccntz  33407  rhmimaidl  33686  esplymhp  33905  dimval  33938  dimvalfi  33939  txomap  34171  qtophaus  34173  erdszelem7  35624  erdszelem8  35625  mrsub0  35943  mrsubccat  35945  mrsubcn  35946  msubrn  35956  mthmblem  36007  ivthALT  36771  weiunfr  36903  ftc2nc  38278  heibor1lem  38385  aks6d1c4  42818  imacrhmcl  43215  ismrc  43361  relpfrlem  45591  icccncfext  46530  dirkercncflem2  46747  smfpimbor1lem1  47441  imaf1co  49855