Theorem fvelrnb 6922

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 6921	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2847	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6875	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2849	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 235	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3158	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2765	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2768	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 289	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3185	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3644	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 289	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  {cab 2739  ∃wrex 3085  Vcvv 3453  ran crn 5644   Fn wfn 6511  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-iota 6472  df-fun 6518  df-fn 6519  df-fv 6524

This theorem is referenced by:  foelcdmi  6923  chfnrn  7025  rexrn  7063  ralrn  7064  elrnrexdmb  7066  ffnfv  7095  elunirn  7230  isoini  7317  canth  7345  mptcnfimad  7962  reldm  8020  seqomlem2  8416  fipreima  9295  ordiso2  9457  inf0  9570  inf3lem6  9582  noinfep  9609  cantnflem4  9641  infenaleph  10041  isinfcard  10042  dfac5  10079  ackbij1  10187  sornom  10228  fin23lem16  10286  fin23lem21  10290  isf32lem2  10305  fin1a2lem5  10355  itunitc  10372  axdc3lem2  10402  zorn2lem4  10450  cfpwsdom  10536  peano2nn  12216  uzn0  12850  om2uzrani  13959  uzrdgfni  13965  uzin2  15363  unbenlem  16935  vdwlem6  17013  0ram  17047  chnso  18647  imasmnd2  18799  imasgrp2  19088  cycsubmel  19232  ghmqusker  19318  pmtrfrn  19489  pgpssslw  19645  efgsfo  19770  efgrelexlemb  19781  gexex  19884  imasrng  20214  imasring  20366  lindfrn  21861  mpfind  22156  mpfpf1  22402  pf1mpf  22403  2ndcomap  23506  kgenidm  23595  kqreglem1  23789  zfbas  23944  rnelfmlem  24000  rnelfm  24001  fmfnfmlem2  24003  ovolctb  25540  ovolicc2  25572  mbfinf  25715  dvivth  26060  dvne0  26061  aannenlem3  26382  reeff1o  26498  oniso  28352  noseqp1  28372  noseqrdgfn  28387  bdayn0sf1o  28451  dfnns2  28453  uhgr2edg  29366  ushgredgedg  29387  ushgredgedgloop  29389  2pthon3v  30100  rnbra  32267  cnvbraval  32270  pjssdif1i  32335  dfpjop  32342  elpjrn  32350  foresf1o  32663  ressupprn  32853  fsumiunle  32992  mgcf1o  33142  imaslmod  33500  dimkerim  33885  rhmpreimacn  34143  esumfsup  34328  esumiun  34352  onvf1odlem4  35410  msrid  35856  tailfb  36698  indexdom  38194  cdleme50rnlem  41129  diaelrnN  41630  diaintclN  41643  cdlemm10N  41703  dibintclN  41752  dihglb2  41927  dihintcl  41929  lcfrlem9  42135  mapd1o  42233  hdmaprnlem11N  42445  hgmaprnlem4N  42484  sticksstones1  42724  aks6d1c6isolem1  42752  aks6d1c6isolem2  42753  aks6d1c6lem5  42755  unitscyglem1  42773  nacsfix  43254  orbitcl  45494  fvelrnbf  45559  cncmpmax  45573  climinf2lem  46241  stoweidlem27  46562  stoweidlem31  46566  stoweidlem48  46583  stoweidlem59  46594  stirlinglem13  46621  fourierdlem12  46654  fourierdlem41  46683  fourierdlem42  46684  fourierdlem46  46687  fourierdlem48  46689  fourierdlem49  46690  fourierdlem70  46711  fourierdlem71  46712  fourierdlem74  46715  fourierdlem75  46716  fourierdlem102  46743  fourierdlem103  46744  fourierdlem104  46745  fourierdlem114  46755  sge0tsms  46915  sge0sup  46926  sge0le  46942  sge0isum  46962  sge0seq  46981  nnfoctbdjlem  46990  meadjiunlem  47000  fcoresf1  47624  iccpartrn  47997  iccpartnel  48005  fmtnorn  48104  isubgredg  48449  gricushgr  48500