Theorem fvelrnb 6969

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 6968	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2825	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6920	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2827	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3149	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2739	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2742	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3177	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3689	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {cab 2712  ∃wrex 3068  Vcvv 3478  ran crn 5690   Fn wfn 6558  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fn 6566  df-fv 6571

This theorem is referenced by:  foelcdmi  6970  chfnrn  7069  rexrn  7107  ralrn  7108  elrnrexdmb  7110  ffnfv  7139  elunirn  7271  isoini  7358  canth  7385  mptcnfimad  8010  reldm  8068  seqomlem2  8490  fipreima  9396  ordiso2  9553  inf0  9659  inf3lem6  9671  noinfep  9698  cantnflem4  9730  infenaleph  10129  isinfcard  10130  dfac5  10167  ackbij1  10275  sornom  10315  fin23lem16  10373  fin23lem21  10377  isf32lem2  10392  fin1a2lem5  10442  itunitc  10459  axdc3lem2  10489  zorn2lem4  10537  cfpwsdom  10622  peano2nn  12276  uzn0  12893  om2uzrani  13990  uzrdgfni  13996  uzin2  15380  unbenlem  16942  vdwlem6  17020  0ram  17054  imasmnd2  18800  imasgrp2  19086  cycsubmel  19231  ghmqusker  19318  pmtrfrn  19491  pgpssslw  19647  efgsfo  19772  efgrelexlemb  19783  gexex  19886  imasrng  20195  imasring  20344  lindfrn  21859  mpfind  22149  mpfpf1  22371  pf1mpf  22372  2ndcomap  23482  kgenidm  23571  kqreglem1  23765  zfbas  23920  rnelfmlem  23976  rnelfm  23977  fmfnfmlem2  23979  ovolctb  25539  ovolicc2  25571  mbfinf  25714  dvivth  26064  dvne0  26065  aannenlem3  26387  reeff1o  26506  noseqp1  28312  noseqrdgfn  28327  dfnns2  28377  uhgr2edg  29240  ushgredgedg  29261  ushgredgedgloop  29263  2pthon3v  29973  rnbra  32136  cnvbraval  32139  pjssdif1i  32204  dfpjop  32211  elpjrn  32219  foresf1o  32532  ressupprn  32705  fsumiunle  32836  mgcf1o  32978  chnso  32988  imaslmod  33361  dimkerim  33655  rhmpreimacn  33846  esumfsup  34051  esumiun  34075  msrid  35530  tailfb  36360  indexdom  37721  cdleme50rnlem  40527  diaelrnN  41028  diaintclN  41041  cdlemm10N  41101  dibintclN  41150  dihglb2  41325  dihintcl  41327  lcfrlem9  41533  mapd1o  41631  hdmaprnlem11N  41843  hgmaprnlem4N  41882  sticksstones1  42128  aks6d1c6isolem1  42156  aks6d1c6isolem2  42157  aks6d1c6lem5  42159  unitscyglem1  42177  nacsfix  42700  fvelrnbf  44956  cncmpmax  44970  climinf2lem  45662  stoweidlem27  45983  stoweidlem31  45987  stoweidlem48  46004  stoweidlem59  46015  stirlinglem13  46042  fourierdlem12  46075  fourierdlem41  46104  fourierdlem42  46105  fourierdlem46  46108  fourierdlem48  46110  fourierdlem49  46111  fourierdlem70  46132  fourierdlem71  46133  fourierdlem74  46136  fourierdlem75  46137  fourierdlem102  46164  fourierdlem103  46165  fourierdlem104  46166  fourierdlem114  46176  sge0tsms  46336  sge0sup  46347  sge0le  46363  sge0isum  46383  sge0seq  46402  nnfoctbdjlem  46411  meadjiunlem  46421  fcoresf1  47019  iccpartrn  47355  iccpartnel  47363  fmtnorn  47459  isubgredg  47790  gricushgr  47824