MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvelimab Structured version   Visualization version   GIF version

Theorem fvelimab 6961
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.
StepHypRef Expression
1 elex 3492 . . 3 (𝐶 ∈ (𝐹𝐵) → 𝐶 ∈ V)
21anim2i 617 . 2 (((𝐹 Fn 𝐴𝐵𝐴) ∧ 𝐶 ∈ (𝐹𝐵)) → ((𝐹 Fn 𝐴𝐵𝐴) ∧ 𝐶 ∈ V))
3 fvex 6901 . . . . 5 (𝐹𝑥) ∈ V
4 eleq1 2821 . . . . 5 ((𝐹𝑥) = 𝐶 → ((𝐹𝑥) ∈ V ↔ 𝐶 ∈ V))
53, 4mpbii 232 . . . 4 ((𝐹𝑥) = 𝐶𝐶 ∈ V)
65rexlimivw 3151 . . 3 (∃𝑥𝐵 (𝐹𝑥) = 𝐶𝐶 ∈ V)
76anim2i 617 . 2 (((𝐹 Fn 𝐴𝐵𝐴) ∧ ∃𝑥𝐵 (𝐹𝑥) = 𝐶) → ((𝐹 Fn 𝐴𝐵𝐴) ∧ 𝐶 ∈ V))
8 eleq1 2821 . . . . . 6 (𝑦 = 𝐶 → (𝑦 ∈ (𝐹𝐵) ↔ 𝐶 ∈ (𝐹𝐵)))
9 eqeq2 2744 . . . . . . 7 (𝑦 = 𝐶 → ((𝐹𝑥) = 𝑦 ↔ (𝐹𝑥) = 𝐶))
109rexbidv 3178 . . . . . 6 (𝑦 = 𝐶 → (∃𝑥𝐵 (𝐹𝑥) = 𝑦 ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶))
118, 10bibi12d 345 . . . . 5 (𝑦 = 𝐶 → ((𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝑦) ↔ (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶)))
1211imbi2d 340 . . . 4 (𝑦 = 𝐶 → (((𝐹 Fn 𝐴𝐵𝐴) → (𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝑦)) ↔ ((𝐹 Fn 𝐴𝐵𝐴) → (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶))))
13 fnfun 6646 . . . . . 6 (𝐹 Fn 𝐴 → Fun 𝐹)
14 fndm 6649 . . . . . . . 8 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
1514sseq2d 4013 . . . . . . 7 (𝐹 Fn 𝐴 → (𝐵 ⊆ dom 𝐹𝐵𝐴))
1615biimpar 478 . . . . . 6 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵 ⊆ dom 𝐹)
17 dfimafn 6951 . . . . . 6 ((Fun 𝐹𝐵 ⊆ dom 𝐹) → (𝐹𝐵) = {𝑦 ∣ ∃𝑥𝐵 (𝐹𝑥) = 𝑦})
1813, 16, 17syl2an2r 683 . . . . 5 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐹𝐵) = {𝑦 ∣ ∃𝑥𝐵 (𝐹𝑥) = 𝑦})
1918eqabrd 2876 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → (𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝑦))
2012, 19vtoclg 3556 . . 3 (𝐶 ∈ V → ((𝐹 Fn 𝐴𝐵𝐴) → (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶)))
2120impcom 408 . 2 (((𝐹 Fn 𝐴𝐵𝐴) ∧ 𝐶 ∈ V) → (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶))
222, 7, 21pm5.21nd 800 1 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  {cab 2709  wrex 3070  Vcvv 3474  wss 3947  dom cdm 5675  cima 5678  Fun wfun 6534   Fn wfn 6535  cfv 6540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-fv 6548
This theorem is referenced by:  fvelimabd  6962  unima  6963  ssimaex  6973  rexima  7235  ralima  7236  f1elima  7258  fnssintima  7355  imaeqsexv  7356  ovelimab  7581  fimaproj  8117  tcrank  9875  djuun  9917  ackbij2  10234  fin1a2lem6  10396  iunfo  10530  grothomex  10820  axpre-sup  11160  injresinjlem  13748  txkgen  23147  fmucndlem  23787  efopn  26157  nocvxmin  27269  eqscut2  27296  cuteq0  27322  elold  27353  lrrecfr  27416  negsproplem2  27492  negsunif  27518  pjimai  31416  fimarab  31855  qtophaus  32804  indf1ofs  33012  eulerpartgbij  33359  eulerpartlemgvv  33363  ballotlemsima  33502  elmthm  34555  elintfv  34724  isnacs2  41429  isnacs3  41433  islmodfg  41796  kercvrlsm  41810  isnumbasgrplem2  41831  dfacbasgrp  41835  fourierdlem62  44870
  Copyright terms: Public domain W3C validator