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

Theorem fvelrnb 6432
Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995.)
Assertion
Ref Expression
fvelrnb (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹

Proof of Theorem fvelrnb
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 fnrnfv 6431 . . 3 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
21eleq2d 2830 . 2 (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹𝐵 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)}))
3 fvex 6388 . . . . 5 (𝐹𝑥) ∈ V
4 eleq1 2832 . . . . 5 ((𝐹𝑥) = 𝐵 → ((𝐹𝑥) ∈ V ↔ 𝐵 ∈ V))
53, 4mpbii 224 . . . 4 ((𝐹𝑥) = 𝐵𝐵 ∈ V)
65rexlimivw 3176 . . 3 (∃𝑥𝐴 (𝐹𝑥) = 𝐵𝐵 ∈ V)
7 eqeq1 2769 . . . . 5 (𝑦 = 𝐵 → (𝑦 = (𝐹𝑥) ↔ 𝐵 = (𝐹𝑥)))
8 eqcom 2772 . . . . 5 (𝐵 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝐵)
97, 8syl6bb 278 . . . 4 (𝑦 = 𝐵 → (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝐵))
109rexbidv 3199 . . 3 (𝑦 = 𝐵 → (∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵))
116, 10elab3 3513 . 2 (𝐵 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵)
122, 11syl6bb 278 1 (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652  wcel 2155  {cab 2751  wrex 3056  Vcvv 3350  ran crn 5278   Fn wfn 6063  cfv 6068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-iota 6031  df-fun 6070  df-fn 6071  df-fv 6076
This theorem is referenced by:  foelrni  6433  chfnrn  6518  rexrn  6551  ralrn  6552  elrnrexdmb  6554  ffnfv  6578  elunirn  6701  isoini  6780  canth  6800  reldm  7419  seqomlem2  7750  fipreima  8479  ordiso2  8627  inf0  8733  inf3lem6  8745  noinfep  8772  cantnflem4  8804  infenaleph  9165  isinfcard  9166  dfac5  9202  ackbij1  9313  sornom  9352  fin23lem16  9410  fin23lem21  9414  isf32lem2  9429  fin1a2lem5  9479  itunitc  9496  axdc3lem2  9526  zorn2lem4  9574  cfpwsdom  9659  peano2nn  11288  uzn0  11902  om2uzrani  12959  uzrdgfni  12965  uzin2  14369  unbenlem  15891  vdwlem6  15969  0ram  16003  imasmnd2  17593  imasgrp2  17797  pmtrfrn  18141  pgpssslw  18293  efgsfo  18417  efgrelexlemb  18429  gexex  18522  imasring  18886  mpfind  19809  mpfpf1  19988  pf1mpf  19989  lindfrn  20436  2ndcomap  21541  kgenidm  21630  kqreglem1  21824  zfbas  21979  rnelfmlem  22035  rnelfm  22036  fmfnfmlem2  22038  ovolctb  23548  ovolicc2  23580  mbfinf  23723  dvivth  24064  dvne0  24065  aannenlem3  24376  reeff1o  24492  uhgr2edg  26378  ushgredgedg  26399  ushgredgedgloop  26401  ushgredgedgloopOLD  26402  2pthon3v  27166  rnbra  29422  cnvbraval  29425  pjssdif1i  29490  dfpjop  29497  elpjrn  29505  foresf1o  29792  fsumiunle  30024  esumfsup  30579  esumiun  30603  msrid  31890  tailfb  32815  cnfinltrel  33674  indexdom  33952  cdleme50rnlem  36500  diaelrnN  37001  diaintclN  37014  cdlemm10N  37074  dibintclN  37123  dihglb2  37298  dihintcl  37300  lcfrlem9  37506  mapd1o  37604  hdmaprnlem11N  37816  hgmaprnlem4N  37855  nacsfix  37953  fvelrnbf  39829  cncmpmax  39843  climinf2lem  40576  stoweidlem27  40881  stoweidlem31  40885  stoweidlem48  40902  stoweidlem59  40913  stirlinglem13  40940  fourierdlem12  40973  fourierdlem41  41002  fourierdlem42  41003  fourierdlem46  41006  fourierdlem48  41008  fourierdlem49  41009  fourierdlem70  41030  fourierdlem71  41031  fourierdlem74  41034  fourierdlem75  41035  fourierdlem102  41062  fourierdlem103  41063  fourierdlem104  41064  fourierdlem114  41074  sge0tsms  41234  sge0sup  41245  sge0le  41261  sge0isum  41281  sge0seq  41300  nnfoctbdjlem  41309  meadjiunlem  41319  iccpartrn  42100  iccpartnel  42108  fmtnorn  42122
  Copyright terms: Public domain W3C validator