Theorem fvelrnb 6894

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 6893	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2822	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6847	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2824	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3133	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2740	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2743	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3160	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3641	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {cab 2714  ∃wrex 3060  Vcvv 3440  ran crn 5625   Fn wfn 6487  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  foelcdmi  6895  chfnrn  6994  rexrn  7032  ralrn  7033  elrnrexdmb  7035  ffnfv  7064  elunirn  7197  isoini  7284  canth  7312  mptcnfimad  7930  reldm  7988  seqomlem2  8382  fipreima  9258  ordiso2  9420  inf0  9530  inf3lem6  9542  noinfep  9569  cantnflem4  9601  infenaleph  10001  isinfcard  10002  dfac5  10039  ackbij1  10147  sornom  10187  fin23lem16  10245  fin23lem21  10249  isf32lem2  10264  fin1a2lem5  10314  itunitc  10331  axdc3lem2  10361  zorn2lem4  10409  cfpwsdom  10495  peano2nn  12157  uzn0  12768  om2uzrani  13875  uzrdgfni  13881  uzin2  15268  unbenlem  16836  vdwlem6  16914  0ram  16948  chnso  18547  imasmnd2  18699  imasgrp2  18985  cycsubmel  19129  ghmqusker  19216  pmtrfrn  19387  pgpssslw  19543  efgsfo  19668  efgrelexlemb  19679  gexex  19782  imasrng  20112  imasring  20266  lindfrn  21776  mpfind  22070  mpfpf1  22295  pf1mpf  22296  2ndcomap  23402  kgenidm  23491  kqreglem1  23685  zfbas  23840  rnelfmlem  23896  rnelfm  23897  fmfnfmlem2  23899  ovolctb  25447  ovolicc2  25479  mbfinf  25622  dvivth  25971  dvne0  25972  aannenlem3  26294  reeff1o  26413  oniso  28267  noseqp1  28287  noseqrdgfn  28302  bdayn0sf1o  28366  dfnns2  28368  uhgr2edg  29281  ushgredgedg  29302  ushgredgedgloop  29304  2pthon3v  30016  rnbra  32182  cnvbraval  32185  pjssdif1i  32250  dfpjop  32257  elpjrn  32265  foresf1o  32579  ressupprn  32769  fsumiunle  32910  mgcf1o  33085  imaslmod  33434  dimkerim  33784  rhmpreimacn  34042  esumfsup  34227  esumiun  34251  onvf1odlem4  35300  msrid  35739  tailfb  36571  indexdom  37935  cdleme50rnlem  40804  diaelrnN  41305  diaintclN  41318  cdlemm10N  41378  dibintclN  41427  dihglb2  41602  dihintcl  41604  lcfrlem9  41810  mapd1o  41908  hdmaprnlem11N  42120  hgmaprnlem4N  42159  sticksstones1  42400  aks6d1c6isolem1  42428  aks6d1c6isolem2  42429  aks6d1c6lem5  42431  unitscyglem1  42449  nacsfix  42954  orbitcl  45198  fvelrnbf  45263  cncmpmax  45277  climinf2lem  45950  stoweidlem27  46271  stoweidlem31  46275  stoweidlem48  46292  stoweidlem59  46303  stirlinglem13  46330  fourierdlem12  46363  fourierdlem41  46392  fourierdlem42  46393  fourierdlem46  46396  fourierdlem48  46398  fourierdlem49  46399  fourierdlem70  46420  fourierdlem71  46421  fourierdlem74  46424  fourierdlem75  46425  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  sge0tsms  46624  sge0sup  46635  sge0le  46651  sge0isum  46671  sge0seq  46690  nnfoctbdjlem  46699  meadjiunlem  46709  fcoresf1  47315  iccpartrn  47676  iccpartnel  47684  fmtnorn  47780  isubgredg  48112  gricushgr  48163