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

Theorem fvelrnb 6904
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 6903 . . 3 (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)})
21eleq2d 2820 . 2 (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹𝐵 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)}))
3 fvex 6856 . . . . 5 (𝐹𝑥) ∈ V
4 eleq1 2822 . . . . 5 ((𝐹𝑥) = 𝐵 → ((𝐹𝑥) ∈ V ↔ 𝐵 ∈ V))
53, 4mpbii 232 . . . 4 ((𝐹𝑥) = 𝐵𝐵 ∈ V)
65rexlimivw 3145 . . 3 (∃𝑥𝐴 (𝐹𝑥) = 𝐵𝐵 ∈ V)
7 eqeq1 2737 . . . . 5 (𝑦 = 𝐵 → (𝑦 = (𝐹𝑥) ↔ 𝐵 = (𝐹𝑥)))
8 eqcom 2740 . . . . 5 (𝐵 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝐵)
97, 8bitrdi 287 . . . 4 (𝑦 = 𝐵 → (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝐵))
109rexbidv 3172 . . 3 (𝑦 = 𝐵 → (∃𝑥𝐴 𝑦 = (𝐹𝑥) ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵))
116, 10elab3 3639 . 2 (𝐵 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = (𝐹𝑥)} ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵)
122, 11bitrdi 287 1 (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥𝐴 (𝐹𝑥) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wcel 2107  {cab 2710  wrex 3070  Vcvv 3444  ran crn 5635   Fn wfn 6492  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fn 6500  df-fv 6505
This theorem is referenced by:  foelcdmi  6905  chfnrn  7000  rexrn  7038  ralrn  7039  elrnrexdmb  7041  ffnfv  7067  elunirn  7199  isoini  7284  canth  7311  reldm  7977  seqomlem2  8398  fipreima  9305  ordiso2  9456  inf0  9562  inf3lem6  9574  noinfep  9601  cantnflem4  9633  infenaleph  10032  isinfcard  10033  dfac5  10069  ackbij1  10179  sornom  10218  fin23lem16  10276  fin23lem21  10280  isf32lem2  10295  fin1a2lem5  10345  itunitc  10362  axdc3lem2  10392  zorn2lem4  10440  cfpwsdom  10525  peano2nn  12170  uzn0  12785  om2uzrani  13863  uzrdgfni  13869  uzin2  15235  unbenlem  16785  vdwlem6  16863  0ram  16897  imasmnd2  18598  imasgrp2  18867  cycsubmel  18998  pmtrfrn  19245  pgpssslw  19401  efgsfo  19526  efgrelexlemb  19537  gexex  19636  imasring  20050  lindfrn  21243  mpfind  21533  mpfpf1  21733  pf1mpf  21734  2ndcomap  22825  kgenidm  22914  kqreglem1  23108  zfbas  23263  rnelfmlem  23319  rnelfm  23320  fmfnfmlem2  23322  ovolctb  24870  ovolicc2  24902  mbfinf  25045  dvivth  25390  dvne0  25391  aannenlem3  25706  reeff1o  25822  uhgr2edg  28198  ushgredgedg  28219  ushgredgedgloop  28221  2pthon3v  28930  rnbra  31091  cnvbraval  31094  pjssdif1i  31159  dfpjop  31166  elpjrn  31174  foresf1o  31474  ressupprn  31651  fsumiunle  31774  mgcf1o  31912  imaslmod  32192  ghmqusker  32246  dimkerim  32379  rhmpreimacn  32523  esumfsup  32726  esumiun  32750  msrid  34196  tailfb  34895  indexdom  36239  cdleme50rnlem  39053  diaelrnN  39554  diaintclN  39567  cdlemm10N  39627  dibintclN  39676  dihglb2  39851  dihintcl  39853  lcfrlem9  40059  mapd1o  40157  hdmaprnlem11N  40369  hgmaprnlem4N  40408  sticksstones1  40600  nacsfix  41078  fvelrnbf  43311  cncmpmax  43325  climinf2lem  44033  stoweidlem27  44354  stoweidlem31  44358  stoweidlem48  44375  stoweidlem59  44386  stirlinglem13  44413  fourierdlem12  44446  fourierdlem41  44475  fourierdlem42  44476  fourierdlem46  44479  fourierdlem48  44481  fourierdlem49  44482  fourierdlem70  44503  fourierdlem71  44504  fourierdlem74  44507  fourierdlem75  44508  fourierdlem102  44535  fourierdlem103  44536  fourierdlem104  44537  fourierdlem114  44547  sge0tsms  44707  sge0sup  44718  sge0le  44734  sge0isum  44754  sge0seq  44773  nnfoctbdjlem  44782  meadjiunlem  44792  fcoresf1  45389  iccpartrn  45708  iccpartnel  45716  fmtnorn  45812  isomushgr  46104
  Copyright terms: Public domain W3C validator