Theorem fvelrnb 6812

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 6811	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2824	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6769	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2826	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 232	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3210	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2742	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2745	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 286	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3225	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3610	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 286	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  {cab 2715  ∃wrex 3064  Vcvv 3422  ran crn 5581   Fn wfn 6413  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-fv 6426

This theorem is referenced by:  foelrni  6813  chfnrn  6908  rexrn  6945  ralrn  6946  elrnrexdmb  6948  ffnfv  6974  elunirn  7106  isoini  7189  canth  7209  reldm  7858  seqomlem2  8252  fipreima  9055  ordiso2  9204  inf0  9309  inf3lem6  9321  noinfep  9348  cantnflem4  9380  infenaleph  9778  isinfcard  9779  dfac5  9815  ackbij1  9925  sornom  9964  fin23lem16  10022  fin23lem21  10026  isf32lem2  10041  fin1a2lem5  10091  itunitc  10108  axdc3lem2  10138  zorn2lem4  10186  cfpwsdom  10271  peano2nn  11915  uzn0  12528  om2uzrani  13600  uzrdgfni  13606  uzin2  14984  unbenlem  16537  vdwlem6  16615  0ram  16649  imasmnd2  18337  imasgrp2  18605  cycsubmel  18734  pmtrfrn  18981  pgpssslw  19134  efgsfo  19260  efgrelexlemb  19271  gexex  19369  imasring  19773  lindfrn  20938  mpfind  21227  mpfpf1  21427  pf1mpf  21428  2ndcomap  22517  kgenidm  22606  kqreglem1  22800  zfbas  22955  rnelfmlem  23011  rnelfm  23012  fmfnfmlem2  23014  ovolctb  24559  ovolicc2  24591  mbfinf  24734  dvivth  25079  dvne0  25080  aannenlem3  25395  reeff1o  25511  uhgr2edg  27478  ushgredgedg  27499  ushgredgedgloop  27501  2pthon3v  28209  rnbra  30370  cnvbraval  30373  pjssdif1i  30438  dfpjop  30445  elpjrn  30453  foresf1o  30751  ressupprn  30926  fsumiunle  31045  mgcf1o  31183  imaslmod  31455  dimkerim  31610  rhmpreimacn  31737  esumfsup  31938  esumiun  31962  msrid  33407  tailfb  34493  indexdom  35819  cdleme50rnlem  38485  diaelrnN  38986  diaintclN  38999  cdlemm10N  39059  dibintclN  39108  dihglb2  39283  dihintcl  39285  lcfrlem9  39491  mapd1o  39589  hdmaprnlem11N  39801  hgmaprnlem4N  39840  sticksstones1  40030  nacsfix  40450  fvelrnbf  42450  cncmpmax  42464  climinf2lem  43137  stoweidlem27  43458  stoweidlem31  43462  stoweidlem48  43479  stoweidlem59  43490  stirlinglem13  43517  fourierdlem12  43550  fourierdlem41  43579  fourierdlem42  43580  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem70  43607  fourierdlem71  43608  fourierdlem74  43611  fourierdlem75  43612  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  sge0tsms  43808  sge0sup  43819  sge0le  43835  sge0isum  43855  sge0seq  43874  nnfoctbdjlem  43883  meadjiunlem  43893  fcoresf1  44450  iccpartrn  44770  iccpartnel  44778  fmtnorn  44874  isomushgr  45166