Theorem fvelimab 6960

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 3479	. . 3 ⊢ (𝐶 ∈ (𝐹 “ 𝐵) → 𝐶 ∈ V)
2	1	anim2i 629	. 2 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ (𝐹 “ 𝐵)) → ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ V))
3		fvex 6901	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2854	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐶 → ((𝐹‘𝑥) ∈ V ↔ 𝐶 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐶 → 𝐶 ∈ V)
6	5	rexlimivw 3165	. . 3 ⊢ (∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶 → 𝐶 ∈ V)
7	6	anim2i 629	. 2 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶) → ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝐶 ∈ V))
8		eleq1 2854	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ (𝐹 “ 𝐵) ↔ 𝐶 ∈ (𝐹 “ 𝐵)))
9		eqeq2 2778	. . . . . . 7 ⊢ (𝑦 = 𝐶 → ((𝐹‘𝑥) = 𝑦 ↔ (𝐹‘𝑥) = 𝐶))
10	9	rexbidv 3192	. . . . . 6 ⊢ (𝑦 = 𝐶 → (∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦 ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))
11	8, 10	bibi12d 348	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦) ↔ (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)))
12	11	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝐶 → (((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦)) ↔ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶))))
13		fnfun 6642	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
14		fndm 6645	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
15	14	sseq2d 3972	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴))
16	15	biimpar 483	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ dom 𝐹)
17		dfimafn 6950	. . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝐵 ⊆ dom 𝐹) → (𝐹 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦})
18	13, 16, 17	syl2an2r 698	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐹 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦})
19	18	eqabrd 2907	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝑦))
20	12, 19	vtoclg 3525	. . 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 2146  {cab 2744  ∃wrex 3092  Vcvv 3458   ⊆ wss 3908  dom cdm 5666   “ cima 5669  Fun wfun 6537   Fn wfn 6538  ‘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-nul 5274  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-ne 2962  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-fn 6546  df-fv 6551

This theorem is used by:  fvelimabd  6961  fimarab  6962  unima  6963  ssimaex  6973  ralima  7242  reximaOLD  7244  ralimaOLD  7245  f1elima  7268  fnssintima  7373  imaeqsexvOLD  7374  ovelimab  7601  fimaproj  8140  tcrank  9866  djuun  9931  ackbij2  10244  fin1a2lem6  10407  iunfo  10541  grothomex  10832  axpre-sup  11172  injresinjlem  13838  txkgen  23846  fmucndlem  24484  efopn  26860  nobdaymin  27983  eqcuts2  28016  cuteq0  28045  elold  28089  lrrecfr  28173  negsproplem2  28259  negsunif  28285  negleft  28288  negright  28289  bdayons  28506  renegscl  28728  pjimai  32565  indf1ofs  33223  qtophaus  34257  eulerpartgbij  34794  eulerpartlemgvv  34798  ballotlemsima  34938  noinfepfnregs  35569  elmthm  36089  elintfv  36278  regsfromunir1  37092  aks6d1c6lem5  42985  isnacs2  43478  isnacs3  43482  islmodfg  43837  kercvrlsm  43851  isnumbasgrplem2  43872  dfacbasgrp  43876  fourierdlem62  46923  uhgrimisgrgric  48737  clnbgrgrim  48740