Theorem fvelrnb 6894

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 6893	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2823	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6847	. . . . 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 3630	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  ∃wrex 3062  Vcvv 3430  ran crn 5625   Fn wfn 6487  ‘cfv 6492

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 5231  ax-nul 5241  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  foelcdmi  6895  chfnrn  6995  rexrn  7033  ralrn  7034  elrnrexdmb  7036  ffnfv  7065  elunirn  7199  isoini  7286  canth  7314  mptcnfimad  7932  reldm  7990  seqomlem2  8383  fipreima  9261  ordiso2  9423  inf0  9533  inf3lem6  9545  noinfep  9572  cantnflem4  9604  infenaleph  10004  isinfcard  10005  dfac5  10042  ackbij1  10150  sornom  10190  fin23lem16  10248  fin23lem21  10252  isf32lem2  10267  fin1a2lem5  10317  itunitc  10334  axdc3lem2  10364  zorn2lem4  10412  cfpwsdom  10498  peano2nn  12177  uzn0  12796  om2uzrani  13905  uzrdgfni  13911  uzin2  15298  unbenlem  16870  vdwlem6  16948  0ram  16982  chnso  18581  imasmnd2  18733  imasgrp2  19022  cycsubmel  19166  ghmqusker  19253  pmtrfrn  19424  pgpssslw  19580  efgsfo  19705  efgrelexlemb  19716  gexex  19819  imasrng  20149  imasring  20301  lindfrn  21811  mpfind  22103  mpfpf1  22326  pf1mpf  22327  2ndcomap  23433  kgenidm  23522  kqreglem1  23716  zfbas  23871  rnelfmlem  23927  rnelfm  23928  fmfnfmlem2  23930  ovolctb  25467  ovolicc2  25499  mbfinf  25642  dvivth  25987  dvne0  25988  aannenlem3  26307  reeff1o  26425  oniso  28277  noseqp1  28297  noseqrdgfn  28312  bdayn0sf1o  28376  dfnns2  28378  uhgr2edg  29291  ushgredgedg  29312  ushgredgedgloop  29314  2pthon3v  30026  rnbra  32193  cnvbraval  32196  pjssdif1i  32261  dfpjop  32268  elpjrn  32276  foresf1o  32589  ressupprn  32778  fsumiunle  32917  mgcf1o  33078  imaslmod  33428  dimkerim  33787  rhmpreimacn  34045  esumfsup  34230  esumiun  34254  onvf1odlem4  35304  msrid  35743  tailfb  36575  indexdom  38069  cdleme50rnlem  41004  diaelrnN  41505  diaintclN  41518  cdlemm10N  41578  dibintclN  41627  dihglb2  41802  dihintcl  41804  lcfrlem9  42010  mapd1o  42108  hdmaprnlem11N  42320  hgmaprnlem4N  42359  sticksstones1  42599  aks6d1c6isolem1  42627  aks6d1c6isolem2  42628  aks6d1c6lem5  42630  unitscyglem1  42648  nacsfix  43158  orbitcl  45402  fvelrnbf  45467  cncmpmax  45481  climinf2lem  46152  stoweidlem27  46473  stoweidlem31  46477  stoweidlem48  46494  stoweidlem59  46505  stirlinglem13  46532  fourierdlem12  46565  fourierdlem41  46594  fourierdlem42  46595  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem70  46622  fourierdlem71  46623  fourierdlem74  46626  fourierdlem75  46627  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem114  46666  sge0tsms  46826  sge0sup  46837  sge0le  46853  sge0isum  46873  sge0seq  46892  nnfoctbdjlem  46901  meadjiunlem  46911  fcoresf1  47529  iccpartrn  47902  iccpartnel  47910  fmtnorn  48009  isubgredg  48354  gricushgr  48405