Theorem fvelima 6948

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃wrex 3089   class class class wbr 5110   “ cima 5666  Fun wfun 6532  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is referenced by:  funimassd  6949  ssimaex  6968  isofrlem  7340  fimaproj  8132  tz7.49  8433  rankwflemb  9766  tcrank  9857  zorn2lem5  10485  zorn2lem6  10486  uniimadom  10529  wunr1om  10705  tskr1om  10753  tskr1om2  10754  grur1  10806  imadrhmcl  20881  iscldtop  23233  kqfvima  23868  fmfnfmlem4  24095  fmfnfm  24096  qustgpopn  24258  cphsscph  25391  c1liplem1  26136  plypf1  26350  lrrecfr  28117  ltgseg  28846  axcontlem9  29303  uhgrspan1  29634  pthdlem2lem  30097  htthlem  31250  xrofsup  33093  tocyccntz  33445  rhmimaidl  33721  esplymhp  33939  dimval  33972  dimvalfi  33973  txomap  34205  qtophaus  34207  erdszelem7  35670  erdszelem8  35671  mrsub0  35989  mrsubccat  35991  mrsubcn  35992  msubrn  36002  mthmblem  36053  ivthALT  36827  weiunfr  36959  ftc2nc  38334  heibor1lem  38441  aks6d1c4  42872  imacrhmcl  43269  ismrc  43415  relpfrlem  45645  icccncfext  46584  dirkercncflem2  46801  smfpimbor1lem1  47495  imaf1co  49916