Theorem fvelima 6723

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃wrex 3071   class class class wbr 5035   “ cima 5530  Fun wfun 6333  ‘cfv 6339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fv 6347

This theorem is referenced by:  ssimaex  6741  isofrlem  7092  fimaproj  7839  tz7.49  8096  rankwflemb  9260  tcrank  9351  zorn2lem5  9965  zorn2lem6  9966  uniimadom  10009  wunr1om  10184  tskr1om  10232  tskr1om2  10233  grur1  10285  iscldtop  21800  kqfvima  22435  fmfnfmlem4  22662  fmfnfm  22663  qustgpopn  22825  cphsscph  23956  c1liplem1  24700  plypf1  24913  ltgseg  26494  axcontlem9  26870  uhgrspan1  27197  pthdlem2lem  27660  htthlem  28804  xrofsup  30618  tocyccntz  30941  rhmimaidl  31134  dimval  31211  dimvalfi  31212  txomap  31309  qtophaus  31311  erdszelem7  32679  erdszelem8  32680  mrsub0  32998  mrsubccat  33000  mrsubcn  33001  msubrn  33011  mthmblem  33062  lrrecfr  33674  ivthALT  34099  ftc2nc  35445  heibor1lem  35553  ismrc  40043  funimassd  42259  icccncfext  42923  dirkercncflem2  43140  smfpimbor1lem1  43824