Theorem fvelima 6895

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3057   class class class wbr 5095   “ cima 5624  Fun wfun 6482  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fv 6496

This theorem is referenced by:  funimassd  6896  ssimaex  6915  isofrlem  7282  fimaproj  8073  tz7.49  8372  rankwflemb  9695  tcrank  9786  zorn2lem5  10400  zorn2lem6  10401  uniimadom  10444  wunr1om  10619  tskr1om  10667  tskr1om2  10668  grur1  10720  imadrhmcl  20716  iscldtop  23013  kqfvima  23648  fmfnfmlem4  23875  fmfnfm  23876  qustgpopn  24038  cphsscph  25181  c1liplem1  25931  plypf1  26147  lrrecfr  27889  ltgseg  28577  axcontlem9  28954  uhgrspan1  29285  pthdlem2lem  29749  htthlem  30901  xrofsup  32756  tocyccntz  33122  rhmimaidl  33406  esplymhp  33610  dimval  33636  dimvalfi  33637  txomap  33870  qtophaus  33872  erdszelem7  35264  erdszelem8  35265  mrsub0  35583  mrsubccat  35585  mrsubcn  35586  msubrn  35596  mthmblem  35647  ivthALT  36402  weiunfr  36534  ftc2nc  37765  heibor1lem  37872  aks6d1c4  42240  imacrhmcl  42635  ismrc  42821  relpfrlem  45073  icccncfext  46012  dirkercncflem2  46229  smfpimbor1lem1  46923  imaf1co  49283