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

Theorem fvelrnb 6725
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 6724 . . 3 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
21eleq2d 2898 . 2 (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹𝐵 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)}))
3 fvex 6682 . . . . 5 (𝐹𝑥) ∈ V
4 eleq1 2900 . . . . 5 ((𝐹𝑥) = 𝐵 → ((𝐹𝑥) ∈ V ↔ 𝐵 ∈ V))
53, 4mpbii 235 . . . 4 ((𝐹𝑥) = 𝐵𝐵 ∈ V)
65rexlimivw 3282 . . 3 (∃𝑥𝐴 (𝐹𝑥) = 𝐵𝐵 ∈ V)
7 eqeq1 2825 . . . . 5 (𝑦 = 𝐵 → (𝑦 = (𝐹𝑥) ↔ 𝐵 = (𝐹𝑥)))
8 eqcom 2828 . . . . 5 (𝐵 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝐵)
97, 8syl6bb 289 . . . 4 (𝑦 = 𝐵 → (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝐵))
109rexbidv 3297 . . 3 (𝑦 = 𝐵 → (∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵))
116, 10elab3 3673 . 2 (𝐵 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵)
122, 11syl6bb 289 1 (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1533  wcel 2110  {cab 2799  wrex 3139  Vcvv 3494  ran crn 5555   Fn wfn 6349  cfv 6354
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-iota 6313  df-fun 6356  df-fn 6357  df-fv 6362
This theorem is referenced by:  foelrni  6726  chfnrn  6818  rexrn  6852  ralrn  6853  elrnrexdmb  6855  ffnfv  6881  elunirn  7009  isoini  7090  canth  7110  reldm  7742  seqomlem2  8086  fipreima  8829  ordiso2  8978  inf0  9083  inf3lem6  9095  noinfep  9122  cantnflem4  9154  infenaleph  9516  isinfcard  9517  dfac5  9553  ackbij1  9659  sornom  9698  fin23lem16  9756  fin23lem21  9760  isf32lem2  9775  fin1a2lem5  9825  itunitc  9842  axdc3lem2  9872  zorn2lem4  9920  cfpwsdom  10005  peano2nn  11649  uzn0  12259  om2uzrani  13319  uzrdgfni  13325  uzin2  14703  unbenlem  16243  vdwlem6  16321  0ram  16355  imasmnd2  17947  imasgrp2  18213  cycsubmel  18342  pmtrfrn  18585  pgpssslw  18738  efgsfo  18864  efgrelexlemb  18875  gexex  18972  imasring  19368  mpfind  20319  mpfpf1  20513  pf1mpf  20514  lindfrn  20964  2ndcomap  22065  kgenidm  22154  kqreglem1  22348  zfbas  22503  rnelfmlem  22559  rnelfm  22560  fmfnfmlem2  22562  ovolctb  24090  ovolicc2  24122  mbfinf  24265  dvivth  24606  dvne0  24607  aannenlem3  24918  reeff1o  25034  uhgr2edg  26989  ushgredgedg  27010  ushgredgedgloop  27012  2pthon3v  27721  rnbra  29883  cnvbraval  29886  pjssdif1i  29951  dfpjop  29958  elpjrn  29966  foresf1o  30264  fsumiunle  30545  imaslmod  30922  dimkerim  31023  esumfsup  31329  esumiun  31353  msrid  32792  tailfb  33725  indexdom  35008  cdleme50rnlem  37679  diaelrnN  38180  diaintclN  38193  cdlemm10N  38253  dibintclN  38302  dihglb2  38477  dihintcl  38479  lcfrlem9  38685  mapd1o  38783  hdmaprnlem11N  38995  hgmaprnlem4N  39034  nacsfix  39307  fvelrnbf  41273  cncmpmax  41287  climinf2lem  41985  stoweidlem27  42311  stoweidlem31  42315  stoweidlem48  42332  stoweidlem59  42343  stirlinglem13  42370  fourierdlem12  42403  fourierdlem41  42432  fourierdlem42  42433  fourierdlem46  42436  fourierdlem48  42438  fourierdlem49  42439  fourierdlem70  42460  fourierdlem71  42461  fourierdlem74  42464  fourierdlem75  42465  fourierdlem102  42492  fourierdlem103  42493  fourierdlem104  42494  fourierdlem114  42504  sge0tsms  42661  sge0sup  42672  sge0le  42688  sge0isum  42708  sge0seq  42727  nnfoctbdjlem  42736  meadjiunlem  42746  iccpartrn  43589  iccpartnel  43597  fmtnorn  43695  isomushgr  43990
  Copyright terms: Public domain W3C validator