Theorem fvelima 6926

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053   class class class wbr 5107   “ cima 5641  Fun wfun 6505  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  funimassd  6927  ssimaex  6946  isofrlem  7315  fimaproj  8114  tz7.49  8413  rankwflemb  9746  tcrank  9837  zorn2lem5  10453  zorn2lem6  10454  uniimadom  10497  wunr1om  10672  tskr1om  10720  tskr1om2  10721  grur1  10773  imadrhmcl  20706  iscldtop  22982  kqfvima  23617  fmfnfmlem4  23844  fmfnfm  23845  qustgpopn  24007  cphsscph  25151  c1liplem1  25901  plypf1  26117  lrrecfr  27850  ltgseg  28523  axcontlem9  28899  uhgrspan1  29230  pthdlem2lem  29697  htthlem  30846  xrofsup  32690  tocyccntz  33101  rhmimaidl  33403  dimval  33596  dimvalfi  33597  txomap  33824  qtophaus  33826  erdszelem7  35184  erdszelem8  35185  mrsub0  35503  mrsubccat  35505  mrsubcn  35506  msubrn  35516  mthmblem  35567  ivthALT  36323  weiunfr  36455  ftc2nc  37696  heibor1lem  37803  aks6d1c4  42112  imacrhmcl  42502  ismrc  42689  relpfrlem  44943  icccncfext  45885  dirkercncflem2  46102  smfpimbor1lem1  46796  imaf1co  49144