Theorem fvelrnb 6939

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 6938	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2818	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6891	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2820	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 232	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3150	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2735	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2738	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 286	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3177	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3672	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 286	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {cab 2708  ∃wrex 3069  Vcvv 3473  ran crn 5670   Fn wfn 6527  ‘cfv 6532

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 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-iota 6484  df-fun 6534  df-fn 6535  df-fv 6540

This theorem is referenced by:  foelcdmi  6940  chfnrn  7035  rexrn  7073  ralrn  7074  elrnrexdmb  7076  ffnfv  7102  elunirn  7234  isoini  7319  canth  7346  reldm  8012  seqomlem2  8433  fipreima  9341  ordiso2  9492  inf0  9598  inf3lem6  9610  noinfep  9637  cantnflem4  9669  infenaleph  10068  isinfcard  10069  dfac5  10105  ackbij1  10215  sornom  10254  fin23lem16  10312  fin23lem21  10316  isf32lem2  10331  fin1a2lem5  10381  itunitc  10398  axdc3lem2  10428  zorn2lem4  10476  cfpwsdom  10561  peano2nn  12206  uzn0  12821  om2uzrani  13899  uzrdgfni  13905  uzin2  15273  unbenlem  16823  vdwlem6  16901  0ram  16935  imasmnd2  18639  imasgrp2  18912  cycsubmel  19043  pmtrfrn  19290  pgpssslw  19446  efgsfo  19571  efgrelexlemb  19582  gexex  19681  imasring  20098  lindfrn  21309  mpfind  21599  mpfpf1  21799  pf1mpf  21800  2ndcomap  22891  kgenidm  22980  kqreglem1  23174  zfbas  23329  rnelfmlem  23385  rnelfm  23386  fmfnfmlem2  23388  ovolctb  24936  ovolicc2  24968  mbfinf  25111  dvivth  25456  dvne0  25457  aannenlem3  25772  reeff1o  25888  uhgr2edg  28330  ushgredgedg  28351  ushgredgedgloop  28353  2pthon3v  29062  rnbra  31223  cnvbraval  31226  pjssdif1i  31291  dfpjop  31298  elpjrn  31306  foresf1o  31606  ressupprn  31783  fsumiunle  31906  mgcf1o  32044  imaslmod  32330  ghmqusker  32387  dimkerim  32550  rhmpreimacn  32696  esumfsup  32899  esumiun  32923  msrid  34367  tailfb  35066  indexdom  36407  cdleme50rnlem  39220  diaelrnN  39721  diaintclN  39734  cdlemm10N  39794  dibintclN  39843  dihglb2  40018  dihintcl  40020  lcfrlem9  40226  mapd1o  40324  hdmaprnlem11N  40536  hgmaprnlem4N  40575  sticksstones1  40767  nacsfix  41221  fvelrnbf  43473  cncmpmax  43487  climinf2lem  44195  stoweidlem27  44516  stoweidlem31  44520  stoweidlem48  44537  stoweidlem59  44548  stirlinglem13  44575  fourierdlem12  44608  fourierdlem41  44637  fourierdlem42  44638  fourierdlem46  44641  fourierdlem48  44643  fourierdlem49  44644  fourierdlem70  44665  fourierdlem71  44666  fourierdlem74  44669  fourierdlem75  44670  fourierdlem102  44697  fourierdlem103  44698  fourierdlem104  44699  fourierdlem114  44709  sge0tsms  44869  sge0sup  44880  sge0le  44896  sge0isum  44916  sge0seq  44935  nnfoctbdjlem  44944  meadjiunlem  44954  fcoresf1  45551  iccpartrn  45870  iccpartnel  45878  fmtnorn  45974  isomushgr  46266