Theorem fvelrnb 6877

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 6876	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2817	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6830	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2819	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3129	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2735	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2738	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3156	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3637	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {cab 2709  ∃wrex 3056  Vcvv 3436  ran crn 5612   Fn wfn 6471  ‘cfv 6476

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-iota 6432  df-fun 6478  df-fn 6479  df-fv 6484

This theorem is referenced by:  foelcdmi  6878  chfnrn  6977  rexrn  7015  ralrn  7016  elrnrexdmb  7018  ffnfv  7047  elunirn  7180  isoini  7267  canth  7295  mptcnfimad  7913  reldm  7971  seqomlem2  8365  fipreima  9237  ordiso2  9396  inf0  9506  inf3lem6  9518  noinfep  9545  cantnflem4  9577  infenaleph  9977  isinfcard  9978  dfac5  10015  ackbij1  10123  sornom  10163  fin23lem16  10221  fin23lem21  10225  isf32lem2  10240  fin1a2lem5  10290  itunitc  10307  axdc3lem2  10337  zorn2lem4  10385  cfpwsdom  10470  peano2nn  12132  uzn0  12744  om2uzrani  13854  uzrdgfni  13860  uzin2  15247  unbenlem  16815  vdwlem6  16893  0ram  16927  chnso  18525  imasmnd2  18677  imasgrp2  18963  cycsubmel  19107  ghmqusker  19194  pmtrfrn  19365  pgpssslw  19521  efgsfo  19646  efgrelexlemb  19657  gexex  19760  imasrng  20090  imasring  20243  lindfrn  21753  mpfind  22037  mpfpf1  22261  pf1mpf  22262  2ndcomap  23368  kgenidm  23457  kqreglem1  23651  zfbas  23806  rnelfmlem  23862  rnelfm  23863  fmfnfmlem2  23865  ovolctb  25413  ovolicc2  25445  mbfinf  25588  dvivth  25937  dvne0  25938  aannenlem3  26260  reeff1o  26379  onsiso  28200  noseqp1  28216  noseqrdgfn  28231  bdayn0sf1o  28290  dfnns2  28292  uhgr2edg  29181  ushgredgedg  29202  ushgredgedgloop  29204  2pthon3v  29916  rnbra  32079  cnvbraval  32082  pjssdif1i  32147  dfpjop  32154  elpjrn  32162  foresf1o  32476  ressupprn  32663  fsumiunle  32804  mgcf1o  32976  imaslmod  33310  dimkerim  33632  rhmpreimacn  33890  esumfsup  34075  esumiun  34099  onvf1odlem4  35142  msrid  35581  tailfb  36411  indexdom  37774  cdleme50rnlem  40583  diaelrnN  41084  diaintclN  41097  cdlemm10N  41157  dibintclN  41206  dihglb2  41381  dihintcl  41383  lcfrlem9  41589  mapd1o  41687  hdmaprnlem11N  41899  hgmaprnlem4N  41938  sticksstones1  42179  aks6d1c6isolem1  42207  aks6d1c6isolem2  42208  aks6d1c6lem5  42210  unitscyglem1  42228  nacsfix  42745  orbitcl  44990  fvelrnbf  45055  cncmpmax  45069  climinf2lem  45744  stoweidlem27  46065  stoweidlem31  46069  stoweidlem48  46086  stoweidlem59  46097  stirlinglem13  46124  fourierdlem12  46157  fourierdlem41  46186  fourierdlem42  46187  fourierdlem46  46190  fourierdlem48  46192  fourierdlem49  46193  fourierdlem70  46214  fourierdlem71  46215  fourierdlem74  46218  fourierdlem75  46219  fourierdlem102  46246  fourierdlem103  46247  fourierdlem104  46248  fourierdlem114  46258  sge0tsms  46418  sge0sup  46429  sge0le  46445  sge0isum  46465  sge0seq  46484  nnfoctbdjlem  46493  meadjiunlem  46503  fcoresf1  47100  iccpartrn  47461  iccpartnel  47469  fmtnorn  47565  isubgredg  47897  gricushgr  47948