Theorem fvelima 6936

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ∃wrex 3089   class class class wbr 5104   “ cima 5654  Fun wfun 6519  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fv 6533

This theorem is referenced by:  funimassd  6937  ssimaex  6956  isofrlem  7328  fimaproj  8119  tz7.49  8420  rankwflemb  9753  tcrank  9844  zorn2lem5  10472  zorn2lem6  10473  uniimadom  10516  wunr1om  10692  tskr1om  10740  tskr1om2  10741  grur1  10793  imadrhmcl  20866  iscldtop  23209  kqfvima  23844  fmfnfmlem4  24071  fmfnfm  24072  qustgpopn  24234  cphsscph  25367  c1liplem1  26112  plypf1  26326  lrrecfr  28090  ltgseg  28819  axcontlem9  29227  uhgrspan1  29558  pthdlem2lem  30021  htthlem  31174  xrofsup  33020  tocyccntz  33372  rhmimaidl  33651  esplymhp  33870  dimval  33903  dimvalfi  33904  txomap  34136  qtophaus  34138  erdszelem7  35555  erdszelem8  35556  mrsub0  35874  mrsubccat  35876  mrsubcn  35877  msubrn  35887  mthmblem  35938  ivthALT  36703  weiunfr  36835  ftc2nc  38208  heibor1lem  38315  aks6d1c4  42748  imacrhmcl  43143  ismrc  43289  relpfrlem  45521  icccncfext  46460  dirkercncflem2  46677  smfpimbor1lem1  47371  imaf1co  49785