Theorem fvelrnb 6726

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 6725	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2898	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6683	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2900	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 235	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3282	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2825	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2828	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	syl6bb 289	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3297	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3674	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	syl6bb 289	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {cab 2799  ∃wrex 3139  Vcvv 3494  ran crn 5556   Fn wfn 6350  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-iota 6314  df-fun 6357  df-fn 6358  df-fv 6363

This theorem is referenced by:  foelrni  6727  chfnrn  6819  rexrn  6853  ralrn  6854  elrnrexdmb  6856  ffnfv  6882  elunirn  7010  isoini  7091  canth  7111  reldm  7743  seqomlem2  8087  fipreima  8830  ordiso2  8979  inf0  9084  inf3lem6  9096  noinfep  9123  cantnflem4  9155  infenaleph  9517  isinfcard  9518  dfac5  9554  ackbij1  9660  sornom  9699  fin23lem16  9757  fin23lem21  9761  isf32lem2  9776  fin1a2lem5  9826  itunitc  9843  axdc3lem2  9873  zorn2lem4  9921  cfpwsdom  10006  peano2nn  11650  uzn0  12261  om2uzrani  13321  uzrdgfni  13327  uzin2  14704  unbenlem  16244  vdwlem6  16322  0ram  16356  imasmnd2  17948  imasgrp2  18214  cycsubmel  18343  pmtrfrn  18586  pgpssslw  18739  efgsfo  18865  efgrelexlemb  18876  gexex  18973  imasring  19369  mpfind  20320  mpfpf1  20514  pf1mpf  20515  lindfrn  20965  2ndcomap  22066  kgenidm  22155  kqreglem1  22349  zfbas  22504  rnelfmlem  22560  rnelfm  22561  fmfnfmlem2  22563  ovolctb  24091  ovolicc2  24123  mbfinf  24266  dvivth  24607  dvne0  24608  aannenlem3  24919  reeff1o  25035  uhgr2edg  26990  ushgredgedg  27011  ushgredgedgloop  27013  2pthon3v  27722  rnbra  29884  cnvbraval  29887  pjssdif1i  29952  dfpjop  29959  elpjrn  29967  foresf1o  30265  fsumiunle  30545  imaslmod  30922  dimkerim  31023  esumfsup  31329  esumiun  31353  msrid  32792  tailfb  33725  indexdom  35024  cdleme50rnlem  37695  diaelrnN  38196  diaintclN  38209  cdlemm10N  38269  dibintclN  38318  dihglb2  38493  dihintcl  38495  lcfrlem9  38701  mapd1o  38799  hdmaprnlem11N  39011  hgmaprnlem4N  39050  nacsfix  39329  fvelrnbf  41295  cncmpmax  41309  climinf2lem  42007  stoweidlem27  42332  stoweidlem31  42336  stoweidlem48  42353  stoweidlem59  42364  stirlinglem13  42391  fourierdlem12  42424  fourierdlem41  42453  fourierdlem42  42454  fourierdlem46  42457  fourierdlem48  42459  fourierdlem49  42460  fourierdlem70  42481  fourierdlem71  42482  fourierdlem74  42485  fourierdlem75  42486  fourierdlem102  42513  fourierdlem103  42514  fourierdlem104  42515  fourierdlem114  42525  sge0tsms  42682  sge0sup  42693  sge0le  42709  sge0isum  42729  sge0seq  42748  nnfoctbdjlem  42757  meadjiunlem  42767  iccpartrn  43610  iccpartnel  43618  fmtnorn  43716  isomushgr  44011