Theorem fvelrnb 6900

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 6899	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2822	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6853	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2824	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3134	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2740	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2743	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3161	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3629	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2714  ∃wrex 3061  Vcvv 3429  ran crn 5632   Fn wfn 6493  ‘cfv 6498

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-fv 6506

This theorem is referenced by:  foelcdmi  6901  chfnrn  7001  rexrn  7039  ralrn  7040  elrnrexdmb  7042  ffnfv  7071  elunirn  7206  isoini  7293  canth  7321  mptcnfimad  7939  reldm  7997  seqomlem2  8390  fipreima  9268  ordiso2  9430  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  12186  uzn0  12805  om2uzrani  13914  uzrdgfni  13920  uzin2  15307  unbenlem  16879  vdwlem6  16957  0ram  16991  chnso  18590  imasmnd2  18742  imasgrp2  19031  cycsubmel  19175  ghmqusker  19262  pmtrfrn  19433  pgpssslw  19589  efgsfo  19714  efgrelexlemb  19725  gexex  19828  imasrng  20158  imasring  20310  lindfrn  21801  mpfind  22093  mpfpf1  22316  pf1mpf  22317  2ndcomap  23423  kgenidm  23512  kqreglem1  23706  zfbas  23861  rnelfmlem  23917  rnelfm  23918  fmfnfmlem2  23920  ovolctb  25457  ovolicc2  25489  mbfinf  25632  dvivth  25977  dvne0  25978  aannenlem3  26296  reeff1o  26412  oniso  28263  noseqp1  28283  noseqrdgfn  28298  bdayn0sf1o  28362  dfnns2  28364  uhgr2edg  29277  ushgredgedg  29298  ushgredgedgloop  29300  2pthon3v  30011  rnbra  32178  cnvbraval  32181  pjssdif1i  32246  dfpjop  32253  elpjrn  32261  foresf1o  32574  ressupprn  32763  fsumiunle  32902  mgcf1o  33063  imaslmod  33413  dimkerim  33771  rhmpreimacn  34029  esumfsup  34214  esumiun  34238  onvf1odlem4  35288  msrid  35727  tailfb  36559  indexdom  38055  cdleme50rnlem  40990  diaelrnN  41491  diaintclN  41504  cdlemm10N  41564  dibintclN  41613  dihglb2  41788  dihintcl  41790  lcfrlem9  41996  mapd1o  42094  hdmaprnlem11N  42306  hgmaprnlem4N  42345  sticksstones1  42585  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  aks6d1c6lem5  42616  unitscyglem1  42634  nacsfix  43144  orbitcl  45384  fvelrnbf  45449  cncmpmax  45463  climinf2lem  46134  stoweidlem27  46455  stoweidlem31  46459  stoweidlem48  46476  stoweidlem59  46487  stirlinglem13  46514  fourierdlem12  46547  fourierdlem41  46576  fourierdlem42  46577  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem70  46604  fourierdlem71  46605  fourierdlem74  46608  fourierdlem75  46609  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  sge0tsms  46808  sge0sup  46819  sge0le  46835  sge0isum  46855  sge0seq  46874  nnfoctbdjlem  46883  meadjiunlem  46893  fcoresf1  47517  iccpartrn  47890  iccpartnel  47898  fmtnorn  47997  isubgredg  48342  gricushgr  48393