Theorem fvelrnb 6952

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 6951	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2819	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6904	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2821	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 232	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3151	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2736	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2739	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 286	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3178	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3676	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 286	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {cab 2709  ∃wrex 3070  Vcvv 3474  ran crn 5677   Fn wfn 6538  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-fv 6551

This theorem is referenced by:  foelcdmi  6953  chfnrn  7050  rexrn  7088  ralrn  7089  elrnrexdmb  7091  ffnfv  7117  elunirn  7249  isoini  7334  canth  7361  reldm  8029  seqomlem2  8450  fipreima  9357  ordiso2  9509  inf0  9615  inf3lem6  9627  noinfep  9654  cantnflem4  9686  infenaleph  10085  isinfcard  10086  dfac5  10122  ackbij1  10232  sornom  10271  fin23lem16  10329  fin23lem21  10333  isf32lem2  10348  fin1a2lem5  10398  itunitc  10415  axdc3lem2  10445  zorn2lem4  10493  cfpwsdom  10578  peano2nn  12223  uzn0  12838  om2uzrani  13916  uzrdgfni  13922  uzin2  15290  unbenlem  16840  vdwlem6  16918  0ram  16952  imasmnd2  18661  imasgrp2  18937  cycsubmel  19076  pmtrfrn  19325  pgpssslw  19481  efgsfo  19606  efgrelexlemb  19617  gexex  19720  imasring  20142  lindfrn  21375  mpfind  21669  mpfpf1  21869  pf1mpf  21870  2ndcomap  22961  kgenidm  23050  kqreglem1  23244  zfbas  23399  rnelfmlem  23455  rnelfm  23456  fmfnfmlem2  23458  ovolctb  25006  ovolicc2  25038  mbfinf  25181  dvivth  25526  dvne0  25527  aannenlem3  25842  reeff1o  25958  uhgr2edg  28462  ushgredgedg  28483  ushgredgedgloop  28485  2pthon3v  29194  rnbra  31355  cnvbraval  31358  pjssdif1i  31423  dfpjop  31430  elpjrn  31438  foresf1o  31737  ressupprn  31907  fsumiunle  32030  mgcf1o  32168  imaslmod  32463  ghmqusker  32527  dimkerim  32707  rhmpreimacn  32860  esumfsup  33063  esumiun  33087  msrid  34531  tailfb  35257  indexdom  36597  cdleme50rnlem  39410  diaelrnN  39911  diaintclN  39924  cdlemm10N  39984  dibintclN  40033  dihglb2  40208  dihintcl  40210  lcfrlem9  40416  mapd1o  40514  hdmaprnlem11N  40726  hgmaprnlem4N  40765  sticksstones1  40957  nacsfix  41440  fvelrnbf  43692  cncmpmax  43706  climinf2lem  44412  stoweidlem27  44733  stoweidlem31  44737  stoweidlem48  44754  stoweidlem59  44765  stirlinglem13  44792  fourierdlem12  44825  fourierdlem41  44854  fourierdlem42  44855  fourierdlem46  44858  fourierdlem48  44860  fourierdlem49  44861  fourierdlem70  44882  fourierdlem71  44883  fourierdlem74  44886  fourierdlem75  44887  fourierdlem102  44914  fourierdlem103  44915  fourierdlem104  44916  fourierdlem114  44926  sge0tsms  45086  sge0sup  45097  sge0le  45113  sge0isum  45133  sge0seq  45152  nnfoctbdjlem  45161  meadjiunlem  45171  fcoresf1  45769  iccpartrn  46088  iccpartnel  46096  fmtnorn  46192  isomushgr  46484  imasrng  46668