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

Theorem fvelrnb 6138
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 6137 . . 3 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
21eleq2d 2673 . 2 (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹𝐵 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)}))
3 fvex 6098 . . . . 5 (𝐹𝑥) ∈ V
4 eleq1 2676 . . . . 5 ((𝐹𝑥) = 𝐵 → ((𝐹𝑥) ∈ V ↔ 𝐵 ∈ V))
53, 4mpbii 222 . . . 4 ((𝐹𝑥) = 𝐵𝐵 ∈ V)
65rexlimivw 3011 . . 3 (∃𝑥𝐴 (𝐹𝑥) = 𝐵𝐵 ∈ V)
7 eqeq1 2614 . . . . 5 (𝑦 = 𝐵 → (𝑦 = (𝐹𝑥) ↔ 𝐵 = (𝐹𝑥)))
8 eqcom 2617 . . . . 5 (𝐵 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝐵)
97, 8syl6bb 275 . . . 4 (𝑦 = 𝐵 → (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝐵))
109rexbidv 3034 . . 3 (𝑦 = 𝐵 → (∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵))
116, 10elab3 3327 . 2 (𝐵 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵)
122, 11syl6bb 275 1 (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  wcel 1977  {cab 2596  wrex 2897  Vcvv 3173  ran crn 5029   Fn wfn 5785  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-iota 5754  df-fun 5792  df-fn 5793  df-fv 5798
This theorem is referenced by:  foelrni  6139  chfnrn  6221  rexrn  6254  ralrn  6255  elrnrexdmb  6257  ffnfv  6280  elunirn  6391  isoini  6466  canth  6486  reldm  7088  seqomlem2  7411  fipreima  8133  ordiso2  8281  inf0  8379  inf3lem6  8391  noinfep  8418  cantnflem4  8450  infenaleph  8775  isinfcard  8776  dfac5  8812  ackbij1  8921  sornom  8960  fin23lem16  9018  fin23lem21  9022  isf32lem2  9037  fin1a2lem5  9087  itunitc  9104  axdc3lem2  9134  zorn2lem4  9182  cfpwsdom  9263  peano2nn  10882  uzn0  11538  om2uzrani  12571  uzrdgfni  12577  uzin2  13881  unbenlem  15399  vdwlem6  15477  0ram  15511  imasmnd2  17099  imasgrp2  17302  pmtrfrn  17650  pgpssslw  17801  efgsfo  17924  efgrelexlemb  17935  gexex  18028  imasring  18391  mpfind  19306  mpfpf1  19485  pf1mpf  19486  lindfrn  19927  2ndcomap  21019  kgenidm  21108  kqreglem1  21302  zfbas  21458  rnelfmlem  21514  rnelfm  21515  fmfnfmlem2  21517  ovolctb  23010  ovolicc2  23042  mbfinf  23183  dvivth  23522  dvne0  23523  aannenlem3  23834  reeff1o  23950  usgraedgrn  25704  usgra2edg  25705  usgrarnedg  25707  vdn0frgrav2  26344  vdgn0frgrav2  26345  rnbra  28144  cnvbraval  28147  pjssdif1i  28212  dfpjop  28219  elpjrn  28227  foresf1o  28521  esumfsup  29253  esumiun  29277  msrid  30490  tailfb  31336  indexdom  32493  cdleme50rnlem  34644  diaelrnN  35146  diaintclN  35159  cdlemm10N  35219  dibintclN  35268  dihglb2  35443  dihintcl  35445  lcfrlem9  35651  mapd1o  35749  hdmaprnlem11N  35964  hgmaprnlem4N  36003  nacsfix  36087  fvelrnbf  37994  cncmpmax  38008  stoweidlem27  38714  stoweidlem31  38718  stoweidlem48  38735  stoweidlem59  38746  stirlinglem13  38773  fourierdlem12  38806  fourierdlem41  38835  fourierdlem42  38836  fourierdlem46  38839  fourierdlem48  38841  fourierdlem49  38842  fourierdlem70  38863  fourierdlem71  38864  fourierdlem74  38867  fourierdlem75  38868  fourierdlem102  38895  fourierdlem103  38896  fourierdlem104  38897  fourierdlem114  38907  sge0tsms  39067  sge0sup  39078  sge0le  39094  sge0isum  39114  sge0seq  39133  nnfoctbdjlem  39142  meadjiunlem  39152  iccpartrn  39763  iccpartnel  39771  fmtnorn  39779  uhgr2edg  40427  ushgredgedga  40448  ushgredgedgaloop  40450  2pthon3v-av  41142
  Copyright terms: Public domain W3C validator