Theorem fvelrnb 6282

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 6281	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2716	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6239	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2718	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 223	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3058	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2655	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2658	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	syl6bb 276	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3081	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3390	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	syl6bb 276	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523   ∈ wcel 2030  {cab 2637  ∃wrex 2942  Vcvv 3231  ran crn 5144   Fn wfn 5921  ‘cfv 5926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-iota 5889  df-fun 5928  df-fn 5929  df-fv 5934

This theorem is referenced by:  foelrni  6283  chfnrn  6368  rexrn  6401  ralrn  6402  elrnrexdmb  6404  ffnfv  6428  elunirn  6549  isoini  6628  canth  6648  reldm  7263  seqomlem2  7591  fipreima  8313  ordiso2  8461  inf0  8556  inf3lem6  8568  noinfep  8595  cantnflem4  8627  infenaleph  8952  isinfcard  8953  dfac5  8989  ackbij1  9098  sornom  9137  fin23lem16  9195  fin23lem21  9199  isf32lem2  9214  fin1a2lem5  9264  itunitc  9281  axdc3lem2  9311  zorn2lem4  9359  cfpwsdom  9444  peano2nn  11070  uzn0  11741  om2uzrani  12791  uzrdgfni  12797  uzin2  14128  unbenlem  15659  vdwlem6  15737  0ram  15771  imasmnd2  17374  imasgrp2  17577  pmtrfrn  17924  pgpssslw  18075  efgsfo  18198  efgrelexlemb  18209  gexex  18302  imasring  18665  mpfind  19584  mpfpf1  19763  pf1mpf  19764  lindfrn  20208  2ndcomap  21309  kgenidm  21398  kqreglem1  21592  zfbas  21747  rnelfmlem  21803  rnelfm  21804  fmfnfmlem2  21806  ovolctb  23304  ovolicc2  23336  mbfinf  23477  dvivth  23818  dvne0  23819  aannenlem3  24130  reeff1o  24246  uhgr2edg  26145  ushgredgedg  26166  ushgredgedgloop  26168  2pthon3v  26908  rnbra  29094  cnvbraval  29097  pjssdif1i  29162  dfpjop  29169  elpjrn  29177  foresf1o  29469  fsumiunle  29703  esumfsup  30260  esumiun  30284  msrid  31568  tailfb  32497  indexdom  33659  cdleme50rnlem  36149  diaelrnN  36651  diaintclN  36664  cdlemm10N  36724  dibintclN  36773  dihglb2  36948  dihintcl  36950  lcfrlem9  37156  mapd1o  37254  hdmaprnlem11N  37469  hgmaprnlem4N  37508  nacsfix  37592  fvelrnbf  39491  cncmpmax  39505  climinf2lem  40256  stoweidlem27  40562  stoweidlem31  40566  stoweidlem48  40583  stoweidlem59  40594  stirlinglem13  40621  fourierdlem12  40654  fourierdlem41  40683  fourierdlem42  40684  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem70  40711  fourierdlem71  40712  fourierdlem74  40715  fourierdlem75  40716  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem114  40755  sge0tsms  40915  sge0sup  40926  sge0le  40942  sge0isum  40962  sge0seq  40981  nnfoctbdjlem  40990  meadjiunlem  41000  iccpartrn  41691  iccpartnel  41699  fmtnorn  41771