Theorem fvelima 6974

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 6958	. . 3 ⊢ (Fun 𝐹 → (𝑥𝐹𝐴 → (𝐹‘𝑥) = 𝐴))
2	1	reximdv 3168	. 2 ⊢ (Fun 𝐹 → (∃𝑥 ∈ 𝐵 𝑥𝐹𝐴 → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴))
3		elimag 6084	. . 3 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → (𝐴 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴))
4	3	ibi 267	. 2 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴)
5	2, 4	impel 505	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∃wrex 3068   class class class wbr 5148   “ cima 5692  Fun wfun 6557  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fv 6571

This theorem is referenced by:  funimassd  6975  ssimaex  6994  isofrlem  7360  fimaproj  8159  tz7.49  8484  rankwflemb  9831  tcrank  9922  zorn2lem5  10538  zorn2lem6  10539  uniimadom  10582  wunr1om  10757  tskr1om  10805  tskr1om2  10806  grur1  10858  imadrhmcl  20815  iscldtop  23119  kqfvima  23754  fmfnfmlem4  23981  fmfnfm  23982  qustgpopn  24144  cphsscph  25299  c1liplem1  26050  plypf1  26266  lrrecfr  27991  ltgseg  28619  axcontlem9  29002  uhgrspan1  29335  pthdlem2lem  29800  htthlem  30946  xrofsup  32778  tocyccntz  33147  rhmimaidl  33440  dimval  33628  dimvalfi  33629  txomap  33795  qtophaus  33797  erdszelem7  35182  erdszelem8  35183  mrsub0  35501  mrsubccat  35503  mrsubcn  35504  msubrn  35514  mthmblem  35565  ivthALT  36318  weiunfr  36450  ftc2nc  37689  heibor1lem  37796  aks6d1c4  42106  imacrhmcl  42501  ismrc  42689  icccncfext  45843  dirkercncflem2  46060  smfpimbor1lem1  46754