Theorem fvelrnb 6895

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {cab 2715  ∃wrex 3061  Vcvv 3441  ran crn 5626   Fn wfn 6488  ‘cfv 6493

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 5242  ax-nul 5252  ax-pr 5378

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fn 6496  df-fv 6501

This theorem is referenced by:  foelcdmi  6896  chfnrn  6996  rexrn  7034  ralrn  7035  elrnrexdmb  7037  ffnfv  7066  elunirn  7199  isoini  7286  canth  7314  mptcnfimad  7932  reldm  7990  seqomlem2  8384  fipreima  9262  ordiso2  9424  inf0  9534  inf3lem6  9546  noinfep  9573  cantnflem4  9605  infenaleph  10005  isinfcard  10006  dfac5  10043  ackbij1  10151  sornom  10191  fin23lem16  10249  fin23lem21  10253  isf32lem2  10268  fin1a2lem5  10318  itunitc  10335  axdc3lem2  10365  zorn2lem4  10413  cfpwsdom  10499  peano2nn  12161  uzn0  12772  om2uzrani  13879  uzrdgfni  13885  uzin2  15272  unbenlem  16840  vdwlem6  16918  0ram  16952  chnso  18551  imasmnd2  18703  imasgrp2  18989  cycsubmel  19133  ghmqusker  19220  pmtrfrn  19391  pgpssslw  19547  efgsfo  19672  efgrelexlemb  19683  gexex  19786  imasrng  20116  imasring  20270  lindfrn  21780  mpfind  22074  mpfpf1  22299  pf1mpf  22300  2ndcomap  23406  kgenidm  23495  kqreglem1  23689  zfbas  23844  rnelfmlem  23900  rnelfm  23901  fmfnfmlem2  23903  ovolctb  25451  ovolicc2  25483  mbfinf  25626  dvivth  25975  dvne0  25976  aannenlem3  26298  reeff1o  26417  onsiso  28252  noseqp1  28272  noseqrdgfn  28287  bdayn0sf1o  28349  dfnns2  28351  uhgr2edg  29264  ushgredgedg  29285  ushgredgedgloop  29287  2pthon3v  29999  rnbra  32165  cnvbraval  32168  pjssdif1i  32233  dfpjop  32240  elpjrn  32248  foresf1o  32561  ressupprn  32750  fsumiunle  32891  mgcf1o  33066  imaslmod  33415  dimkerim  33765  rhmpreimacn  34023  esumfsup  34208  esumiun  34232  onvf1odlem4  35281  msrid  35720  tailfb  36552  indexdom  37906  cdleme50rnlem  40841  diaelrnN  41342  diaintclN  41355  cdlemm10N  41415  dibintclN  41464  dihglb2  41639  dihintcl  41641  lcfrlem9  41847  mapd1o  41945  hdmaprnlem11N  42157  hgmaprnlem4N  42196  sticksstones1  42437  aks6d1c6isolem1  42465  aks6d1c6isolem2  42466  aks6d1c6lem5  42468  unitscyglem1  42486  nacsfix  42990  orbitcl  45234  fvelrnbf  45299  cncmpmax  45313  climinf2lem  45986  stoweidlem27  46307  stoweidlem31  46311  stoweidlem48  46328  stoweidlem59  46339  stirlinglem13  46366  fourierdlem12  46399  fourierdlem41  46428  fourierdlem42  46429  fourierdlem46  46432  fourierdlem48  46434  fourierdlem49  46435  fourierdlem70  46456  fourierdlem71  46457  fourierdlem74  46460  fourierdlem75  46461  fourierdlem102  46488  fourierdlem103  46489  fourierdlem104  46490  fourierdlem114  46500  sge0tsms  46660  sge0sup  46671  sge0le  46687  sge0isum  46707  sge0seq  46726  nnfoctbdjlem  46735  meadjiunlem  46745  fcoresf1  47351  iccpartrn  47712  iccpartnel  47720  fmtnorn  47816  isubgredg  48148  gricushgr  48199