Theorem fvelrnb 6943

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 6942	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2847	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6896	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2849	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3160	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2765	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2768	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 290	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3187	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3640	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {cab 2739  ∃wrex 3087  Vcvv 3451  ran crn 5652   Fn wfn 6532  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is used by:  foelcdmi  6944  chfnrn  7046  rexrn  7085  ralrn  7086  elrnrexdmb  7088  ffnfv  7117  elunirn  7253  isoini  7344  canth  7372  mptcnfimad  7996  reldm  8053  seqomlem2  8454  fipreima  9340  ordiso2  9502  inf0  9615  inf3lem6  9627  noinfep  9654  cantnflem4  9686  infenaleph  10163  isinfcard  10164  dfac5  10200  ackbij1  10308  sornom  10348  fin23lem16  10406  fin23lem21  10410  isf32lem2  10425  fin1a2lem5  10475  itunitc  10492  axdc3lem2  10522  zorn2lem4  10570  cfpwsdom  10662  peano2nn  12340  uzn0  12975  om2uzrani  14088  uzrdgfni  14094  uzin2  15505  unbenlem  17079  vdwlem6  17157  0ram  17191  chnso  18791  imasmgm2  18856  imasmnd2  18961  imasgrp2  19258  cycsubmel  19408  ghmqusker  19494  pmtrfrn  19665  pgpssslw  19821  efgsfo  19946  efgrelexlemb  19957  gexex  20060  imasrng  20392  imasring  20553  lindfrn  22120  mpfind  22417  mpfpf1  22662  pf1mpf  22663  2ndcomap  23770  kgenidm  23859  kqreglem1  24053  zfbas  24208  rnelfmlem  24264  rnelfm  24265  fmfnfmlem2  24267  ovolctb  25804  ovolicc2  25836  mbfinf  25979  dvivth  26323  dvne0  26324  plyconz  26624  aannenlem3  26650  reeff1o  26767  oniso  28650  noseqp1  28670  noseqrdgfn  28685  bdayn0sf1o  28749  dfnns2  28751  uhgr2edg  29782  ushgredgedg  29803  ushgredgedgloop  29805  2pthon3v  30525  rnbra  32702  cnvbraval  32705  pjssdif1i  32770  dfpjop  32777  elpjrn  32785  foresf1o  33093  ressupprn  33276  fsumiunle  33413  mgcf1o  33557  imaslmod  33907  dimkerim  34252  rhmpreimacn  34510  esumfsup  34695  esumiun  34719  onvf1odlem4  35868  msrid  36289  tailfb  37145  indexdom  38648  cdleme50rnlem  41581  diaelrnN  42082  diaintclN  42095  cdlemm10N  42155  dibintclN  42204  dihglb2  42379  dihintcl  42381  lcfrlem9  42587  mapd1o  42685  hdmaprnlem11N  42897  hgmaprnlem4N  42936  sticksstones1  43176  aks6d1c6isolem1  43204  aks6d1c6isolem2  43205  aks6d1c6lem5  43207  unitscyglem1  43225  nacsfix  43702  orbitcl  45925  fvelrnbf  46004  cncmpmax  46018  climinf2lem  46685  stoweidlem27  47006  stoweidlem31  47010  stoweidlem48  47027  stoweidlem59  47038  stirlinglem13  47065  fourierdlem12  47098  fourierdlem41  47127  fourierdlem42  47128  fourierdlem46  47131  fourierdlem48  47133  fourierdlem49  47134  fourierdlem70  47155  fourierdlem71  47156  fourierdlem74  47159  fourierdlem75  47160  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem114  47199  sge0tsms  47359  sge0sup  47370  sge0le  47386  sge0isum  47406  sge0seq  47425  nnfoctbdjlem  47434  meadjiunlem  47444  fcoresf1  48108  iccpartrn  48481  iccpartnel  48489  fmtnorn  48588  isubgredg  48933  gricushgr  48984