Theorem fvelrnb 6902

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 6901	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2823	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6855	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2825	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3135	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2741	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2744	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3162	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3643	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  ∃wrex 3062  Vcvv 3442  ran crn 5633   Fn wfn 6495  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-fv 6508

This theorem is referenced by:  foelcdmi  6903  chfnrn  7003  rexrn  7041  ralrn  7042  elrnrexdmb  7044  ffnfv  7073  elunirn  7207  isoini  7294  canth  7322  mptcnfimad  7940  reldm  7998  seqomlem2  8392  fipreima  9270  ordiso2  9432  inf0  9542  inf3lem6  9554  noinfep  9581  cantnflem4  9613  infenaleph  10013  isinfcard  10014  dfac5  10051  ackbij1  10159  sornom  10199  fin23lem16  10257  fin23lem21  10261  isf32lem2  10276  fin1a2lem5  10326  itunitc  10343  axdc3lem2  10373  zorn2lem4  10421  cfpwsdom  10507  peano2nn  12169  uzn0  12780  om2uzrani  13887  uzrdgfni  13893  uzin2  15280  unbenlem  16848  vdwlem6  16926  0ram  16960  chnso  18559  imasmnd2  18711  imasgrp2  18997  cycsubmel  19141  ghmqusker  19228  pmtrfrn  19399  pgpssslw  19555  efgsfo  19680  efgrelexlemb  19691  gexex  19794  imasrng  20124  imasring  20278  lindfrn  21788  mpfind  22082  mpfpf1  22307  pf1mpf  22308  2ndcomap  23414  kgenidm  23503  kqreglem1  23697  zfbas  23852  rnelfmlem  23908  rnelfm  23909  fmfnfmlem2  23911  ovolctb  25459  ovolicc2  25491  mbfinf  25634  dvivth  25983  dvne0  25984  aannenlem3  26306  reeff1o  26425  oniso  28279  noseqp1  28299  noseqrdgfn  28314  bdayn0sf1o  28378  dfnns2  28380  uhgr2edg  29293  ushgredgedg  29314  ushgredgedgloop  29316  2pthon3v  30028  rnbra  32195  cnvbraval  32198  pjssdif1i  32263  dfpjop  32270  elpjrn  32278  foresf1o  32591  ressupprn  32780  fsumiunle  32921  mgcf1o  33096  imaslmod  33446  dimkerim  33805  rhmpreimacn  34063  esumfsup  34248  esumiun  34272  onvf1odlem4  35322  msrid  35761  tailfb  36593  indexdom  37985  cdleme50rnlem  40920  diaelrnN  41421  diaintclN  41434  cdlemm10N  41494  dibintclN  41543  dihglb2  41718  dihintcl  41720  lcfrlem9  41926  mapd1o  42024  hdmaprnlem11N  42236  hgmaprnlem4N  42275  sticksstones1  42516  aks6d1c6isolem1  42544  aks6d1c6isolem2  42545  aks6d1c6lem5  42547  unitscyglem1  42565  nacsfix  43069  orbitcl  45313  fvelrnbf  45378  cncmpmax  45392  climinf2lem  46064  stoweidlem27  46385  stoweidlem31  46389  stoweidlem48  46406  stoweidlem59  46417  stirlinglem13  46444  fourierdlem12  46477  fourierdlem41  46506  fourierdlem42  46507  fourierdlem46  46510  fourierdlem48  46512  fourierdlem49  46513  fourierdlem70  46534  fourierdlem71  46535  fourierdlem74  46538  fourierdlem75  46539  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem114  46578  sge0tsms  46738  sge0sup  46749  sge0le  46765  sge0isum  46785  sge0seq  46804  nnfoctbdjlem  46813  meadjiunlem  46823  fcoresf1  47429  iccpartrn  47790  iccpartnel  47798  fmtnorn  47894  isubgredg  48226  gricushgr  48277