Theorem fvelima 6964

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ∈ wcel 2099  ∃wrex 3067   class class class wbr 5148   “ cima 5681  Fun wfun 6542  ‘cfv 6548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fv 6556

This theorem is referenced by:  funimassd  6965  ssimaex  6983  isofrlem  7348  fimaproj  8140  tz7.49  8466  rankwflemb  9817  tcrank  9908  zorn2lem5  10524  zorn2lem6  10525  uniimadom  10568  wunr1om  10743  tskr1om  10791  tskr1om2  10792  grur1  10844  imadrhmcl  20685  iscldtop  23012  kqfvima  23647  fmfnfmlem4  23874  fmfnfm  23875  qustgpopn  24037  cphsscph  25192  c1liplem1  25942  plypf1  26159  lrrecfr  27873  ltgseg  28413  axcontlem9  28796  uhgrspan1  29129  pthdlem2lem  29594  htthlem  30740  xrofsup  32550  tocyccntz  32878  rhmimaidl  33161  dimval  33298  dimvalfi  33299  txomap  33435  qtophaus  33437  erdszelem7  34807  erdszelem8  34808  mrsub0  35126  mrsubccat  35128  mrsubcn  35129  msubrn  35139  mthmblem  35190  ivthALT  35819  ftc2nc  37175  heibor1lem  37282  aks6d1c4  41595  imacrhmcl  41751  ismrc  42121  icccncfext  45275  dirkercncflem2  45492  smfpimbor1lem1  46186

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »