Theorem fvelrnb 6887

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.

Step	Hyp	Ref	Expression
1		fnrnfv 6886	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2825	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6840	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2827	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 234	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3136	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2743	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2746	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 288	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3163	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3624	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 288	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {cab 2717  ∃wrex 3063  Vcvv 3431  ran crn 5619   Fn wfn 6480  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-iota 6441  df-fun 6487  df-fn 6488  df-fv 6493

This theorem is referenced by:  foelcdmi  6888  chfnrn  6990  rexrn  7028  ralrn  7029  elrnrexdmb  7031  ffnfv  7060  elunirn  7195  isoini  7282  canth  7310  mptcnfimad  7928  reldm  7986  seqomlem2  8380  fipreima  9258  ordiso2  9420  inf0  9533  inf3lem6  9545  noinfep  9572  cantnflem4  9604  infenaleph  10004  isinfcard  10005  dfac5  10042  ackbij1  10150  sornom  10190  fin23lem16  10248  fin23lem21  10252  isf32lem2  10267  fin1a2lem5  10317  itunitc  10334  axdc3lem2  10364  zorn2lem4  10412  cfpwsdom  10498  peano2nn  12177  uzn0  12796  om2uzrani  13905  uzrdgfni  13911  uzin2  15298  unbenlem  16870  vdwlem6  16948  0ram  16982  chnso  18581  imasmnd2  18733  imasgrp2  19022  cycsubmel  19166  ghmqusker  19253  pmtrfrn  19424  pgpssslw  19580  efgsfo  19705  efgrelexlemb  19716  gexex  19819  imasrng  20149  imasring  20301  lindfrn  21796  mpfind  22091  mpfpf1  22337  pf1mpf  22338  2ndcomap  23441  kgenidm  23530  kqreglem1  23724  zfbas  23879  rnelfmlem  23935  rnelfm  23936  fmfnfmlem2  23938  ovolctb  25475  ovolicc2  25507  mbfinf  25650  dvivth  25995  dvne0  25996  aannenlem3  26314  reeff1o  26430  oniso  28281  noseqp1  28301  noseqrdgfn  28316  bdayn0sf1o  28380  dfnns2  28382  uhgr2edg  29295  ushgredgedg  29316  ushgredgedgloop  29318  2pthon3v  30029  rnbra  32196  cnvbraval  32199  pjssdif1i  32264  dfpjop  32271  elpjrn  32279  foresf1o  32592  ressupprn  32782  fsumiunle  32921  mgcf1o  33082  imaslmod  33436  dimkerim  33811  rhmpreimacn  34069  esumfsup  34254  esumiun  34278  onvf1odlem4  35334  msrid  35773  tailfb  36605  indexdom  38101  cdleme50rnlem  41036  diaelrnN  41537  diaintclN  41550  cdlemm10N  41610  dibintclN  41659  dihglb2  41834  dihintcl  41836  lcfrlem9  42042  mapd1o  42140  hdmaprnlem11N  42352  hgmaprnlem4N  42391  sticksstones1  42631  aks6d1c6isolem1  42659  aks6d1c6isolem2  42660  aks6d1c6lem5  42662  unitscyglem1  42680  nacsfix  43161  orbitcl  45401  fvelrnbf  45466  cncmpmax  45480  climinf2lem  46149  stoweidlem27  46470  stoweidlem31  46474  stoweidlem48  46491  stoweidlem59  46502  stirlinglem13  46529  fourierdlem12  46562  fourierdlem41  46591  fourierdlem42  46592  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem70  46619  fourierdlem71  46620  fourierdlem74  46623  fourierdlem75  46624  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  sge0tsms  46823  sge0sup  46834  sge0le  46850  sge0isum  46870  sge0seq  46889  nnfoctbdjlem  46898  meadjiunlem  46908  fcoresf1  47532  iccpartrn  47905  iccpartnel  47913  fmtnorn  48012  isubgredg  48357  gricushgr  48408