Theorem fvelrnb 6243

Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995.)

Assertion

Ref	Expression
fvelrnb	|- ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )

Distinct variable groups:   x, A   x, B   x, F

Proof of Theorem fvelrnb

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnrnfv 6242	. . 3 |- ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )
2	1	eleq2d 2687	. 2 |- ( F Fn A -> ( B e. ran F <-> B e. { y | E. x e. A y = ( F ` x ) } ) )
3		fvex 6201	. . . . 5 |- ( F ` x ) e. _V
4		eleq1 2689	. . . . 5 |- ( ( F ` x ) = B -> ( ( F ` x ) e. _V <-> B e. _V ) )
5	3, 4	mpbii 223	. . . 4 |- ( ( F ` x ) = B -> B e. _V )
6	5	rexlimivw 3029	. . 3 |- ( E. x e. A ( F ` x ) = B -> B e. _V )
7		eqeq1 2626	. . . . 5 |- ( y = B -> ( y = ( F ` x ) <-> B = ( F ` x ) ) )
8		eqcom 2629	. . . . 5 |- ( B = ( F ` x ) <-> ( F ` x ) = B )
9	7, 8	syl6bb 276	. . . 4 |- ( y = B -> ( y = ( F ` x ) <-> ( F ` x ) = B ) )
10	9	rexbidv 3052	. . 3 |- ( y = B -> ( E. x e. A y = ( F ` x ) <-> E. x e. A ( F ` x ) = B ) )
11	6, 10	elab3 3358	. 2 |- ( B e. { y | E. x e. A y = ( F ` x ) } <-> E. x e. A ( F ` x ) = B )
12	2, 11	syl6bb 276	1 |- ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   {cab 2608   E.wrex 2913   _Vcvv 3200   ran crn 5115   Fn wfn 5883   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896

This theorem is referenced by:  foelrni  6244  chfnrn  6328  rexrn  6361  ralrn  6362  elrnrexdmb  6364  ffnfv  6388  elunirn  6509  isoini  6588  canth  6608  reldm  7219  seqomlem2  7546  fipreima  8272  ordiso2  8420  inf0  8518  inf3lem6  8530  noinfep  8557  cantnflem4  8589  infenaleph  8914  isinfcard  8915  dfac5  8951  ackbij1  9060  sornom  9099  fin23lem16  9157  fin23lem21  9161  isf32lem2  9176  fin1a2lem5  9226  itunitc  9243  axdc3lem2  9273  zorn2lem4  9321  cfpwsdom  9406  peano2nn  11032  uzn0  11703  om2uzrani  12751  uzrdgfni  12757  uzin2  14084  unbenlem  15612  vdwlem6  15690  0ram  15724  imasmnd2  17327  imasgrp2  17530  pmtrfrn  17878  pgpssslw  18029  efgsfo  18152  efgrelexlemb  18163  gexex  18256  imasring  18619  mpfind  19536  mpfpf1  19715  pf1mpf  19716  lindfrn  20160  2ndcomap  21261  kgenidm  21350  kqreglem1  21544  zfbas  21700  rnelfmlem  21756  rnelfm  21757  fmfnfmlem2  21759  ovolctb  23258  ovolicc2  23290  mbfinf  23432  dvivth  23773  dvne0  23774  aannenlem3  24085  reeff1o  24201  uhgr2edg  26100  ushgredgedg  26121  ushgredgedgloop  26123  2pthon3v  26839  rnbra  28966  cnvbraval  28969  pjssdif1i  29034  dfpjop  29041  elpjrn  29049  foresf1o  29343  fsumiunle  29575  esumfsup  30132  esumiun  30156  msrid  31442  tailfb  32372  indexdom  33529  cdleme50rnlem  35832  diaelrnN  36334  diaintclN  36347  cdlemm10N  36407  dibintclN  36456  dihglb2  36631  dihintcl  36633  lcfrlem9  36839  mapd1o  36937  hdmaprnlem11N  37152  hgmaprnlem4N  37191  nacsfix  37275  fvelrnbf  39177  cncmpmax  39191  climinf2lem  39938  stoweidlem27  40244  stoweidlem31  40248  stoweidlem48  40265  stoweidlem59  40276  stirlinglem13  40303  fourierdlem12  40336  fourierdlem41  40365  fourierdlem42  40366  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem70  40393  fourierdlem71  40394  fourierdlem74  40397  fourierdlem75  40398  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  sge0tsms  40597  sge0sup  40608  sge0le  40624  sge0isum  40644  sge0seq  40663  nnfoctbdjlem  40672  meadjiunlem  40682  iccpartrn  41366  iccpartnel  41374  fmtnorn  41446