Theorem fvelrnb 6953

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 6952	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2820	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6905	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2822	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 232	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3152	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2737	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2740	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3179	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3677	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {cab 2710  ∃wrex 3071  Vcvv 3475  ran crn 5678   Fn wfn 6539  ‘cfv 6544

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 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-fv 6552

This theorem is referenced by:  foelcdmi  6954  chfnrn  7051  rexrn  7089  ralrn  7090  elrnrexdmb  7092  ffnfv  7118  elunirn  7250  isoini  7335  canth  7362  reldm  8030  seqomlem2  8451  fipreima  9358  ordiso2  9510  inf0  9616  inf3lem6  9628  noinfep  9655  cantnflem4  9687  infenaleph  10086  isinfcard  10087  dfac5  10123  ackbij1  10233  sornom  10272  fin23lem16  10330  fin23lem21  10334  isf32lem2  10349  fin1a2lem5  10399  itunitc  10416  axdc3lem2  10446  zorn2lem4  10494  cfpwsdom  10579  peano2nn  12224  uzn0  12839  om2uzrani  13917  uzrdgfni  13923  uzin2  15291  unbenlem  16841  vdwlem6  16919  0ram  16953  imasmnd2  18662  imasgrp2  18938  cycsubmel  19077  pmtrfrn  19326  pgpssslw  19482  efgsfo  19607  efgrelexlemb  19618  gexex  19721  imasring  20143  lindfrn  21376  mpfind  21670  mpfpf1  21870  pf1mpf  21871  2ndcomap  22962  kgenidm  23051  kqreglem1  23245  zfbas  23400  rnelfmlem  23456  rnelfm  23457  fmfnfmlem2  23459  ovolctb  25007  ovolicc2  25039  mbfinf  25182  dvivth  25527  dvne0  25528  aannenlem3  25843  reeff1o  25959  uhgr2edg  28465  ushgredgedg  28486  ushgredgedgloop  28488  2pthon3v  29197  rnbra  31360  cnvbraval  31363  pjssdif1i  31428  dfpjop  31435  elpjrn  31443  foresf1o  31742  ressupprn  31912  fsumiunle  32035  mgcf1o  32173  imaslmod  32468  ghmqusker  32532  dimkerim  32712  rhmpreimacn  32865  esumfsup  33068  esumiun  33092  msrid  34536  tailfb  35262  indexdom  36602  cdleme50rnlem  39415  diaelrnN  39916  diaintclN  39929  cdlemm10N  39989  dibintclN  40038  dihglb2  40213  dihintcl  40215  lcfrlem9  40421  mapd1o  40519  hdmaprnlem11N  40731  hgmaprnlem4N  40770  sticksstones1  40962  nacsfix  41450  fvelrnbf  43702  cncmpmax  43716  climinf2lem  44422  stoweidlem27  44743  stoweidlem31  44747  stoweidlem48  44764  stoweidlem59  44775  stirlinglem13  44802  fourierdlem12  44835  fourierdlem41  44864  fourierdlem42  44865  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem70  44892  fourierdlem71  44893  fourierdlem74  44896  fourierdlem75  44897  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem114  44936  sge0tsms  45096  sge0sup  45107  sge0le  45123  sge0isum  45143  sge0seq  45162  nnfoctbdjlem  45171  meadjiunlem  45181  fcoresf1  45779  iccpartrn  46098  iccpartnel  46106  fmtnorn  46202  isomushgr  46494  imasrng  46678