Theorem fvelrnb 6951

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 6950	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2817	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6903	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2819	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 232	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3149	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2734	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2737	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 286	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3176	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3675	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 286	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104  {cab 2707  ∃wrex 3068  Vcvv 3472  ran crn 5676   Fn wfn 6537  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6494  df-fun 6544  df-fn 6545  df-fv 6550

This theorem is referenced by:  foelcdmi  6952  chfnrn  7049  rexrn  7087  ralrn  7088  elrnrexdmb  7090  ffnfv  7119  elunirn  7252  isoini  7337  canth  7364  reldm  8032  seqomlem2  8453  fipreima  9360  ordiso2  9512  inf0  9618  inf3lem6  9630  noinfep  9657  cantnflem4  9689  infenaleph  10088  isinfcard  10089  dfac5  10125  ackbij1  10235  sornom  10274  fin23lem16  10332  fin23lem21  10336  isf32lem2  10351  fin1a2lem5  10401  itunitc  10418  axdc3lem2  10448  zorn2lem4  10496  cfpwsdom  10581  peano2nn  12228  uzn0  12843  om2uzrani  13921  uzrdgfni  13927  uzin2  15295  unbenlem  16845  vdwlem6  16923  0ram  16957  imasmnd2  18696  imasgrp2  18974  cycsubmel  19115  pmtrfrn  19367  pgpssslw  19523  efgsfo  19648  efgrelexlemb  19659  gexex  19762  imasrng  20071  imasring  20218  lindfrn  21595  mpfind  21889  mpfpf1  22090  pf1mpf  22091  2ndcomap  23182  kgenidm  23271  kqreglem1  23465  zfbas  23620  rnelfmlem  23676  rnelfm  23677  fmfnfmlem2  23679  ovolctb  25239  ovolicc2  25271  mbfinf  25414  dvivth  25762  dvne0  25763  aannenlem3  26079  reeff1o  26195  peano2n0s  27940  uhgr2edg  28732  ushgredgedg  28753  ushgredgedgloop  28755  2pthon3v  29464  rnbra  31627  cnvbraval  31630  pjssdif1i  31695  dfpjop  31702  elpjrn  31710  foresf1o  32009  ressupprn  32179  fsumiunle  32302  mgcf1o  32440  imaslmod  32738  ghmqusker  32806  dimkerim  33000  rhmpreimacn  33163  esumfsup  33366  esumiun  33390  msrid  34834  tailfb  35565  indexdom  36905  cdleme50rnlem  39718  diaelrnN  40219  diaintclN  40232  cdlemm10N  40292  dibintclN  40341  dihglb2  40516  dihintcl  40518  lcfrlem9  40724  mapd1o  40822  hdmaprnlem11N  41034  hgmaprnlem4N  41073  sticksstones1  41268  nacsfix  41752  fvelrnbf  44004  cncmpmax  44018  climinf2lem  44720  stoweidlem27  45041  stoweidlem31  45045  stoweidlem48  45062  stoweidlem59  45073  stirlinglem13  45100  fourierdlem12  45133  fourierdlem41  45162  fourierdlem42  45163  fourierdlem46  45166  fourierdlem48  45168  fourierdlem49  45169  fourierdlem70  45190  fourierdlem71  45191  fourierdlem74  45194  fourierdlem75  45195  fourierdlem102  45222  fourierdlem103  45223  fourierdlem104  45224  fourierdlem114  45234  sge0tsms  45394  sge0sup  45405  sge0le  45421  sge0isum  45441  sge0seq  45460  nnfoctbdjlem  45469  meadjiunlem  45479  fcoresf1  46077  iccpartrn  46396  iccpartnel  46404  fmtnorn  46500  isomushgr  46792