Theorem fvelrnb 6891

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 6890	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2819	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6844	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2821	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3130	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2737	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2740	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3157	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3638	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {cab 2711  ∃wrex 3057  Vcvv 3437  ran crn 5622   Fn wfn 6484  ‘cfv 6489

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 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fn 6492  df-fv 6497

This theorem is referenced by:  foelcdmi  6892  chfnrn  6991  rexrn  7029  ralrn  7030  elrnrexdmb  7032  ffnfv  7061  elunirn  7194  isoini  7281  canth  7309  mptcnfimad  7927  reldm  7985  seqomlem2  8379  fipreima  9253  ordiso2  9412  inf0  9522  inf3lem6  9534  noinfep  9561  cantnflem4  9593  infenaleph  9993  isinfcard  9994  dfac5  10031  ackbij1  10139  sornom  10179  fin23lem16  10237  fin23lem21  10241  isf32lem2  10256  fin1a2lem5  10306  itunitc  10323  axdc3lem2  10353  zorn2lem4  10401  cfpwsdom  10486  peano2nn  12148  uzn0  12759  om2uzrani  13866  uzrdgfni  13872  uzin2  15259  unbenlem  16827  vdwlem6  16905  0ram  16939  chnso  18538  imasmnd2  18690  imasgrp2  18976  cycsubmel  19120  ghmqusker  19207  pmtrfrn  19378  pgpssslw  19534  efgsfo  19659  efgrelexlemb  19670  gexex  19773  imasrng  20103  imasring  20257  lindfrn  21767  mpfind  22061  mpfpf1  22286  pf1mpf  22287  2ndcomap  23393  kgenidm  23482  kqreglem1  23676  zfbas  23831  rnelfmlem  23887  rnelfm  23888  fmfnfmlem2  23890  ovolctb  25438  ovolicc2  25470  mbfinf  25613  dvivth  25962  dvne0  25963  aannenlem3  26285  reeff1o  26404  onsiso  28225  noseqp1  28241  noseqrdgfn  28256  bdayn0sf1o  28315  dfnns2  28317  uhgr2edg  29207  ushgredgedg  29228  ushgredgedgloop  29230  2pthon3v  29942  rnbra  32108  cnvbraval  32111  pjssdif1i  32176  dfpjop  32183  elpjrn  32191  foresf1o  32505  ressupprn  32695  fsumiunle  32838  mgcf1o  33013  imaslmod  33362  dimkerim  33712  rhmpreimacn  33970  esumfsup  34155  esumiun  34179  onvf1odlem4  35222  msrid  35661  tailfb  36493  indexdom  37847  cdleme50rnlem  40716  diaelrnN  41217  diaintclN  41230  cdlemm10N  41290  dibintclN  41339  dihglb2  41514  dihintcl  41516  lcfrlem9  41722  mapd1o  41820  hdmaprnlem11N  42032  hgmaprnlem4N  42071  sticksstones1  42312  aks6d1c6isolem1  42340  aks6d1c6isolem2  42341  aks6d1c6lem5  42343  unitscyglem1  42361  nacsfix  42869  orbitcl  45114  fvelrnbf  45179  cncmpmax  45193  climinf2lem  45866  stoweidlem27  46187  stoweidlem31  46191  stoweidlem48  46208  stoweidlem59  46219  stirlinglem13  46246  fourierdlem12  46279  fourierdlem41  46308  fourierdlem42  46309  fourierdlem46  46312  fourierdlem48  46314  fourierdlem49  46315  fourierdlem70  46336  fourierdlem71  46337  fourierdlem74  46340  fourierdlem75  46341  fourierdlem102  46368  fourierdlem103  46369  fourierdlem104  46370  fourierdlem114  46380  sge0tsms  46540  sge0sup  46551  sge0le  46567  sge0isum  46587  sge0seq  46606  nnfoctbdjlem  46615  meadjiunlem  46625  fcoresf1  47231  iccpartrn  47592  iccpartnel  47600  fmtnorn  47696  isubgredg  48028  gricushgr  48079