Theorem fvelimab 6954

Description: Function value in an image. (Contributed by NM, 20-Jan-2007.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Revised by David Abernethy, 17-Dec-2011.)

Assertion

Ref	Expression
fvelimab	⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))

Distinct variable groups:   𝑥,𝐵   𝑥,𝐶   𝑥,𝐹

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem fvelimab

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3474	. . 3 ⊢ (𝐶 ∈ (𝐹 “ 𝐵) → 𝐶 ∈ V)
2	1	anim2i 629	. 2 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ (𝐹 “ 𝐵)) → ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ V))
3		fvex 6895	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2850	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐶 → ((𝐹‘𝑥) ∈ V ↔ 𝐶 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐶 → 𝐶 ∈ V)
6	5	rexlimivw 3161	. . 3 ⊢ (∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶 → 𝐶 ∈ V)
7	6	anim2i 629	. 2 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶) → ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ V))
8		eleq1 2850	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ (𝐹 “ 𝐵) ↔ 𝐶 ∈ (𝐹 “ 𝐵)))
9		eqeq2 2774	. . . . . . 7 ⊢ (𝑦 = 𝐶 → ((𝐹‘𝑥) = 𝑦 ↔ (𝐹‘𝑥) = 𝐶))
10	9	rexbidv 3188	. . . . . 6 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦 ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))
11	8, 10	bibi12d 348	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦) ↔ (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)))
12	11	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝐶 → (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦)) ↔ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))))
13		fnfun 6636	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
14		fndm 6639	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
15	14	sseq2d 3966	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴))
16	15	biimpar 483	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ dom 𝐹)
17		dfimafn 6944	. . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ dom 𝐹) → (𝐹 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦})
18	13, 16, 17	syl2an2r 698	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦})
19	18	eqabrd 2903	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦))
20	12, 19	vtoclg 3520	. . 3 ⊢ (𝐶 ∈ V → ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)))
21	20	impcom 413	. 2 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ V) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))
22	2, 7, 21	pm5.21nd 814	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2740  ∃wrex 3088  Vcvv 3453   ⊆ wss 3902  dom cdm 5659   “ cima 5662  Fun wfun 6531   Fn wfn 6532  ‘cfv 6537

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 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is used by:  fvelimabd  6955  fimarab  6956  unima  6957  ssimaex  6967  ralima  7240  f1elima  7264  fnssintima  7369  ovelimab  7596  fimaproj  8137  tcrank  9870  djuun  9935  ackbij2  10248  fin1a2lem6  10411  iunfo  10551  grothomex  10842  axpre-sup  11182  injresinjlem  13850  txkgen  23884  fmucndlem  24522  efopn  26903  nobdaymin  28026  eqcuts2  28059  cuteq0  28088  elold  28132  lrrecfr  28216  negsproplem2  28302  negsunif  28328  negleft  28331  negright  28332  bdayons  28549  renegscl  28771  pjimai  32665  indf1ofs  33320  qtophaus  34354  eulerpartgbij  34891  eulerpartlemgvv  34895  ballotlemsima  35035  noinfepfnregs  35666  elmthm  36163  elintfv  36352  regsfromunir1  37167  aks6d1c6lem5  43051  isnacs2  43559  isnacs3  43563  islmodfg  43918  kercvrlsm  43932  isnumbasgrplem2  43953  dfacbasgrp  43957  fourierdlem62  47004  uhgrimisgrgric  48855  clnbgrgrim  48858