Theorem fvelima 6953

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 6936	. . 3 ⊢ (Fun 𝐹 → (𝑥𝐹𝐴 → (𝐹‘𝑥) = 𝐴))
2	1	reximdv 3183	. 2 ⊢ (Fun 𝐹 → (∃𝑥 ∈ 𝐵 𝑥𝐹𝐴 → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴))
3		elimag 6071	. . 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 2146  ∃wrex 3092   class class class wbr 5114   “ cima 5669  Fun wfun 6537  ‘cfv 6543

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 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fv 6551

This theorem is used by:  funimassd  6954  ssimaex  6973  isofrlem  7349  fimaproj  8140  tz7.49  8441  rankwflemb  9775  tcrank  9866  zorn2lem5  10502  zorn2lem6  10503  uniimadom  10546  wunr1om  10722  tskr1om  10770  tskr1om2  10771  grur1  10823  imadrhmcl  20937  iscldtop  23289  kqfvima  23924  fmfnfmlem4  24151  fmfnfm  24152  qustgpopn  24314  cphsscph  25447  c1liplem1  26192  plypf1  26406  lrrecfr  28173  ltgseg  28902  axcontlem9  29359  uhgrspan1  29690  pthdlem2lem  30153  htthlem  31306  xrofsup  33149  tocyccntz  33495  rhmimaidl  33771  esplymhp  33989  dimval  34022  dimvalfi  34023  txomap  34255  qtophaus  34257  erdszelem7  35710  erdszelem8  35711  mrsub0  36029  mrsubccat  36031  mrsubcn  36032  msubrn  36042  mthmblem  36093  ivthALT  36887  weiunfr  37019  ftc2nc  38394  heibor1lem  38501  aks6d1c4  42932  imacrhmcl  43329  ismrc  43473  relpfrlem  45703  icccncfext  46642  dirkercncflem2  46859  smfpimbor1lem1  47553  imaf1co  49974