Theorem fvelrnb 6839

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 6838	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2825	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6796	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2827	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 232	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3212	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2743	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2746	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3227	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3618	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2107  {cab 2716  ∃wrex 3066  Vcvv 3433  ran crn 5591   Fn wfn 6432  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6395  df-fun 6439  df-fn 6440  df-fv 6445

This theorem is referenced by:  foelrni  6840  chfnrn  6935  rexrn  6972  ralrn  6973  elrnrexdmb  6975  ffnfv  7001  elunirn  7133  isoini  7218  canth  7238  reldm  7894  seqomlem2  8291  fipreima  9134  ordiso2  9283  inf0  9388  inf3lem6  9400  noinfep  9427  cantnflem4  9459  infenaleph  9856  isinfcard  9857  dfac5  9893  ackbij1  10003  sornom  10042  fin23lem16  10100  fin23lem21  10104  isf32lem2  10119  fin1a2lem5  10169  itunitc  10186  axdc3lem2  10216  zorn2lem4  10264  cfpwsdom  10349  peano2nn  11994  uzn0  12608  om2uzrani  13681  uzrdgfni  13687  uzin2  15065  unbenlem  16618  vdwlem6  16696  0ram  16730  imasmnd2  18431  imasgrp2  18699  cycsubmel  18828  pmtrfrn  19075  pgpssslw  19228  efgsfo  19354  efgrelexlemb  19365  gexex  19463  imasring  19867  lindfrn  21037  mpfind  21326  mpfpf1  21526  pf1mpf  21527  2ndcomap  22618  kgenidm  22707  kqreglem1  22901  zfbas  23056  rnelfmlem  23112  rnelfm  23113  fmfnfmlem2  23115  ovolctb  24663  ovolicc2  24695  mbfinf  24838  dvivth  25183  dvne0  25184  aannenlem3  25499  reeff1o  25615  uhgr2edg  27584  ushgredgedg  27605  ushgredgedgloop  27607  2pthon3v  28317  rnbra  30478  cnvbraval  30481  pjssdif1i  30546  dfpjop  30553  elpjrn  30561  foresf1o  30859  ressupprn  31033  fsumiunle  31152  mgcf1o  31290  imaslmod  31562  dimkerim  31717  rhmpreimacn  31844  esumfsup  32047  esumiun  32071  msrid  33516  tailfb  34575  indexdom  35901  cdleme50rnlem  38565  diaelrnN  39066  diaintclN  39079  cdlemm10N  39139  dibintclN  39188  dihglb2  39363  dihintcl  39365  lcfrlem9  39571  mapd1o  39669  hdmaprnlem11N  39881  hgmaprnlem4N  39920  sticksstones1  40109  nacsfix  40541  fvelrnbf  42568  cncmpmax  42582  climinf2lem  43254  stoweidlem27  43575  stoweidlem31  43579  stoweidlem48  43596  stoweidlem59  43607  stirlinglem13  43634  fourierdlem12  43667  fourierdlem41  43696  fourierdlem42  43697  fourierdlem46  43700  fourierdlem48  43702  fourierdlem49  43703  fourierdlem70  43724  fourierdlem71  43725  fourierdlem74  43728  fourierdlem75  43729  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem114  43768  sge0tsms  43925  sge0sup  43936  sge0le  43952  sge0isum  43972  sge0seq  43991  nnfoctbdjlem  44000  meadjiunlem  44010  fcoresf1  44574  iccpartrn  44893  iccpartnel  44901  fmtnorn  44997  isomushgr  45289