Theorem fvelrnb 6939

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 6938	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2855	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6892	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2857	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3168	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2773	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2776	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 290	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3195	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3654	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  {cab 2747  ∃wrex 3095  Vcvv 3463  ran crn 5660   Fn wfn 6529  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6490  df-fun 6536  df-fn 6537  df-fv 6542

This theorem is referenced by:  foelcdmi  6940  chfnrn  7042  rexrn  7080  ralrn  7081  elrnrexdmb  7083  ffnfv  7112  elunirn  7247  isoini  7334  canth  7362  mptcnfimad  7979  reldm  8037  seqomlem2  8434  fipreima  9311  ordiso2  9473  inf0  9586  inf3lem6  9598  noinfep  9625  cantnflem4  9657  infenaleph  10071  isinfcard  10072  dfac5  10108  ackbij1  10216  sornom  10257  fin23lem16  10315  fin23lem21  10319  isf32lem2  10334  fin1a2lem5  10384  itunitc  10401  axdc3lem2  10431  zorn2lem4  10479  cfpwsdom  10565  peano2nn  12241  uzn0  12875  om2uzrani  13984  uzrdgfni  13990  uzin2  15392  unbenlem  16964  vdwlem6  17042  0ram  17076  chnso  18676  imasmnd2  18828  imasgrp2  19117  cycsubmel  19267  ghmqusker  19353  pmtrfrn  19524  pgpssslw  19680  efgsfo  19805  efgrelexlemb  19816  gexex  19919  imasrng  20251  imasring  20408  lindfrn  21936  mpfind  22231  mpfpf1  22476  pf1mpf  22477  2ndcomap  23580  kgenidm  23669  kqreglem1  23863  zfbas  24018  rnelfmlem  24074  rnelfm  24075  fmfnfmlem2  24077  ovolctb  25614  ovolicc2  25646  mbfinf  25789  dvivth  26134  dvne0  26135  aannenlem3  26456  reeff1o  26572  oniso  28426  noseqp1  28446  noseqrdgfn  28461  bdayn0sf1o  28525  dfnns2  28527  uhgr2edg  29495  ushgredgedg  29516  ushgredgedgloop  29518  2pthon3v  30229  rnbra  32396  cnvbraval  32399  pjssdif1i  32464  dfpjop  32471  elpjrn  32479  foresf1o  32787  ressupprn  32972  fsumiunle  33110  mgcf1o  33260  imaslmod  33612  dimkerim  33958  rhmpreimacn  34216  esumfsup  34401  esumiun  34425  onvf1odlem4  35485  msrid  35932  tailfb  36773  indexdom  38268  cdleme50rnlem  41203  diaelrnN  41704  diaintclN  41717  cdlemm10N  41777  dibintclN  41826  dihglb2  42001  dihintcl  42003  lcfrlem9  42209  mapd1o  42307  hdmaprnlem11N  42519  hgmaprnlem4N  42558  sticksstones1  42798  aks6d1c6isolem1  42826  aks6d1c6isolem2  42827  aks6d1c6lem5  42829  unitscyglem1  42847  nacsfix  43330  orbitcl  45553  fvelrnbf  45625  cncmpmax  45639  climinf2lem  46307  stoweidlem27  46628  stoweidlem31  46632  stoweidlem48  46649  stoweidlem59  46660  stirlinglem13  46687  fourierdlem12  46720  fourierdlem41  46749  fourierdlem42  46750  fourierdlem46  46753  fourierdlem48  46755  fourierdlem49  46756  fourierdlem70  46777  fourierdlem71  46778  fourierdlem74  46781  fourierdlem75  46782  fourierdlem102  46809  fourierdlem103  46810  fourierdlem104  46811  fourierdlem114  46821  sge0tsms  46981  sge0sup  46992  sge0le  47008  sge0isum  47028  sge0seq  47047  nnfoctbdjlem  47056  meadjiunlem  47066  fcoresf1  47690  iccpartrn  48063  iccpartnel  48071  fmtnorn  48170  isubgredg  48515  gricushgr  48566