Theorem fvelima 6947

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 6930	. . 3 ⊢ (Fun 𝐹 → (𝑥𝐹𝐴 → (𝐹‘𝑥) = 𝐴))
2	1	reximdv 3179	. 2 ⊢ (Fun 𝐹 → (∃𝑥 ∈ 𝐵 𝑥𝐹𝐴 → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴))
3		elimag 6064	. . 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 2145  ∃wrex 3088   class class class wbr 5107   “ cima 5662  Fun wfun 6531  ‘cfv 6537

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  funimassd  6948  ssimaex  6967  isofrlem  7345  fimaproj  8137  tz7.49  8438  rankwflemb  9779  tcrank  9870  zorn2lem5  10506  zorn2lem6  10507  uniimadom  10556  wunr1om  10732  tskr1om  10780  tskr1om2  10781  grur1  10833  imadrhmcl  20969  iscldtop  23326  kqfvima  23962  fmfnfmlem4  24189  fmfnfm  24190  qustgpopn  24352  cphsscph  25485  c1liplem1  26230  plypf1  26445  lrrecfr  28216  ltgseg  28946  axcontlem9  29437  uhgrspan1  29771  pthdlem2lem  30240  htthlem  31406  xrofsup  33246  tocyccntz  33592  rhmimaidl  33868  esplymhp  34086  dimval  34119  dimvalfi  34120  txomap  34352  qtophaus  34354  erdszelem7  35784  erdszelem8  35785  mrsub0  36103  mrsubccat  36105  mrsubcn  36106  msubrn  36116  mthmblem  36167  ivthALT  36962  weiunfr  37094  ftc2nc  38459  heibor1lem  38567  aks6d1c4  42998  imacrhmcl  43410  ismrc  43554  relpfrlem  45784  icccncfext  46723  dirkercncflem2  46940  smfpimbor1lem1  47634  imaf1co  50089