Theorem fvelima 6402

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		elimag 5620	. . . 4 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → (𝐴 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴))
2	1	ibi 256	. . 3 ⊢ (𝐴 ∈ (𝐹 “ 𝐵) → ∃𝑥 ∈ 𝐵 𝑥𝐹𝐴)
3		funbrfv 6387	. . . 4 ⊢ (Fun 𝐹 → (𝑥𝐹𝐴 → (𝐹‘𝑥) = 𝐴))
4	3	reximdv 3146	. . 3 ⊢ (Fun 𝐹 → (∃𝑥 ∈ 𝐵 𝑥𝐹𝐴 → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴))
5	2, 4	syl5 34	. 2 ⊢ (Fun 𝐹 → (𝐴 ∈ (𝐹 “ 𝐵) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴))
6	5	imp 444	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ (𝐹 “ 𝐵)) → ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1624   ∈ wcel 2131  ∃wrex 3043   class class class wbr 4796   “ cima 5261  Fun wfun 6035  ‘cfv 6041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fv 6049

This theorem is referenced by:  ssimaex  6417  isofrlem  6745  tz7.49  7701  rankwflemb  8821  tcrank  8912  zorn2lem5  9506  zorn2lem6  9507  uniimadom  9550  wunr1om  9725  tskr1om  9773  tskr1om2  9774  grur1  9826  iscldtop  21093  kqfvima  21727  fmfnfmlem4  21954  fmfnfm  21955  qustgpopn  22116  c1liplem1  23950  plypf1  24159  ltgseg  25682  axcontlem9  26043  uhgrspan1  26386  pthdlem2lem  26865  htthlem  28075  xrofsup  29834  fimaproj  30201  txomap  30202  qtophaus  30204  erdszelem7  31478  erdszelem8  31479  mrsub0  31712  mrsubccat  31714  mrsubcn  31715  msubrn  31725  mthmblem  31776  ivthALT  32628  ftc2nc  33799  heibor1lem  33913  ismrc  37758  funimassd  39922  icccncfext  40595  dirkercncflem2  40816  smfpimbor1lem1  41503