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

Theorem fvelimab 6397
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 3364 . . 3 (𝐶 ∈ (𝐹𝐵) → 𝐶 ∈ V)
21anim2i 603 . 2 (((𝐹 Fn 𝐴𝐵𝐴) ∧ 𝐶 ∈ (𝐹𝐵)) → ((𝐹 Fn 𝐴𝐵𝐴) ∧ 𝐶 ∈ V))
3 fvex 6344 . . . . 5 (𝐹𝑥) ∈ V
4 eleq1 2838 . . . . 5 ((𝐹𝑥) = 𝐶 → ((𝐹𝑥) ∈ V ↔ 𝐶 ∈ V))
53, 4mpbii 223 . . . 4 ((𝐹𝑥) = 𝐶𝐶 ∈ V)
65rexlimivw 3177 . . 3 (∃𝑥𝐵 (𝐹𝑥) = 𝐶𝐶 ∈ V)
76anim2i 603 . 2 (((𝐹 Fn 𝐴𝐵𝐴) ∧ ∃𝑥𝐵 (𝐹𝑥) = 𝐶) → ((𝐹 Fn 𝐴𝐵𝐴) ∧ 𝐶 ∈ V))
8 eleq1 2838 . . . . . 6 (𝑦 = 𝐶 → (𝑦 ∈ (𝐹𝐵) ↔ 𝐶 ∈ (𝐹𝐵)))
9 eqeq2 2782 . . . . . . 7 (𝑦 = 𝐶 → ((𝐹𝑥) = 𝑦 ↔ (𝐹𝑥) = 𝐶))
109rexbidv 3200 . . . . . 6 (𝑦 = 𝐶 → (∃𝑥𝐵 (𝐹𝑥) = 𝑦 ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶))
118, 10bibi12d 334 . . . . 5 (𝑦 = 𝐶 → ((𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝑦) ↔ (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶)))
1211imbi2d 329 . . . 4 (𝑦 = 𝐶 → (((𝐹 Fn 𝐴𝐵𝐴) → (𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝑦)) ↔ ((𝐹 Fn 𝐴𝐵𝐴) → (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶))))
13 fnfun 6127 . . . . . 6 (𝐹 Fn 𝐴 → Fun 𝐹)
14 fndm 6129 . . . . . . . 8 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
1514sseq2d 3782 . . . . . . 7 (𝐹 Fn 𝐴 → (𝐵 ⊆ dom 𝐹𝐵𝐴))
1615biimpar 463 . . . . . 6 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵 ⊆ dom 𝐹)
17 dfimafn 6389 . . . . . 6 ((Fun 𝐹𝐵 ⊆ dom 𝐹) → (𝐹𝐵) = {𝑦 ∣ ∃𝑥𝐵 (𝐹𝑥) = 𝑦})
1813, 16, 17syl2an2r 664 . . . . 5 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐹𝐵) = {𝑦 ∣ ∃𝑥𝐵 (𝐹𝑥) = 𝑦})
1918abeq2d 2883 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → (𝑦 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝑦))
2012, 19vtoclg 3417 . . 3 (𝐶 ∈ V → ((𝐹 Fn 𝐴𝐵𝐴) → (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶)))
2120impcom 394 . 2 (((𝐹 Fn 𝐴𝐵𝐴) ∧ 𝐶 ∈ V) → (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶))
222, 7, 21pm5.21nd 803 1 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐶 ∈ (𝐹𝐵) ↔ ∃𝑥𝐵 (𝐹𝑥) = 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  {cab 2757  wrex 3062  Vcvv 3351  wss 3723  dom cdm 5250  cima 5253  Fun wfun 6024   Fn wfn 6025  cfv 6030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5993  df-fun 6032  df-fn 6033  df-fv 6038
This theorem is referenced by:  fvelimabd  6398  ssimaex  6407  rexima  6642  ralima  6643  f1elima  6665  ovelimab  6962  tcrank  8914  djuun  8955  ackbij2  9270  fin1a2lem6  9432  iunfo  9566  grothomex  9856  axpre-sup  10195  injresinjlem  12795  lmhmima  19259  txkgen  21675  fmucndlem  22314  mdegldg  24045  ig1peu  24150  efopn  24624  pjimai  29374  fimarab  29784  fimaproj  30239  qtophaus  30242  indf1ofs  30427  eulerpartgbij  30773  eulerpartlemgvv  30777  ballotlemsima  30916  elmthm  31810  nocvxmin  32230  isnacs2  37795  isnacs3  37799  islmodfg  38165  kercvrlsm  38179  isnumbasgrplem2  38200  dfacbasgrp  38204  unima  39865  fourierdlem62  40899
  Copyright terms: Public domain W3C validator