Theorem fvelrnb 6921

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 6920	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2814	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6871	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2816	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3130	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2733	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2736	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3157	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3653	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  ∃wrex 3053  Vcvv 3447  ran crn 5639   Fn wfn 6506  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-fv 6519

This theorem is referenced by:  foelcdmi  6922  chfnrn  7021  rexrn  7059  ralrn  7060  elrnrexdmb  7062  ffnfv  7091  elunirn  7225  isoini  7313  canth  7341  mptcnfimad  7965  reldm  8023  seqomlem2  8419  fipreima  9309  ordiso2  9468  inf0  9574  inf3lem6  9586  noinfep  9613  cantnflem4  9645  infenaleph  10044  isinfcard  10045  dfac5  10082  ackbij1  10190  sornom  10230  fin23lem16  10288  fin23lem21  10292  isf32lem2  10307  fin1a2lem5  10357  itunitc  10374  axdc3lem2  10404  zorn2lem4  10452  cfpwsdom  10537  peano2nn  12198  uzn0  12810  om2uzrani  13917  uzrdgfni  13923  uzin2  15311  unbenlem  16879  vdwlem6  16957  0ram  16991  imasmnd2  18701  imasgrp2  18987  cycsubmel  19132  ghmqusker  19219  pmtrfrn  19388  pgpssslw  19544  efgsfo  19669  efgrelexlemb  19680  gexex  19783  imasrng  20086  imasring  20239  lindfrn  21730  mpfind  22014  mpfpf1  22238  pf1mpf  22239  2ndcomap  23345  kgenidm  23434  kqreglem1  23628  zfbas  23783  rnelfmlem  23839  rnelfm  23840  fmfnfmlem2  23842  ovolctb  25391  ovolicc2  25423  mbfinf  25566  dvivth  25915  dvne0  25916  aannenlem3  26238  reeff1o  26357  onsiso  28169  noseqp1  28185  noseqrdgfn  28200  bdayn0sf1o  28259  dfnns2  28261  uhgr2edg  29135  ushgredgedg  29156  ushgredgedgloop  29158  2pthon3v  29873  rnbra  32036  cnvbraval  32039  pjssdif1i  32104  dfpjop  32111  elpjrn  32119  foresf1o  32433  ressupprn  32613  fsumiunle  32754  mgcf1o  32929  chnso  32940  imaslmod  33324  dimkerim  33623  rhmpreimacn  33875  esumfsup  34060  esumiun  34084  onvf1odlem4  35093  msrid  35532  tailfb  36365  indexdom  37728  cdleme50rnlem  40538  diaelrnN  41039  diaintclN  41052  cdlemm10N  41112  dibintclN  41161  dihglb2  41336  dihintcl  41338  lcfrlem9  41544  mapd1o  41642  hdmaprnlem11N  41854  hgmaprnlem4N  41893  sticksstones1  42134  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  aks6d1c6lem5  42165  unitscyglem1  42183  nacsfix  42700  orbitcl  44947  fvelrnbf  45012  cncmpmax  45026  climinf2lem  45704  stoweidlem27  46025  stoweidlem31  46029  stoweidlem48  46046  stoweidlem59  46057  stirlinglem13  46084  fourierdlem12  46117  fourierdlem41  46146  fourierdlem42  46147  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem70  46174  fourierdlem71  46175  fourierdlem74  46178  fourierdlem75  46179  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  sge0tsms  46378  sge0sup  46389  sge0le  46405  sge0isum  46425  sge0seq  46444  nnfoctbdjlem  46453  meadjiunlem  46463  fcoresf1  47070  iccpartrn  47431  iccpartnel  47439  fmtnorn  47535  isubgredg  47866  gricushgr  47917