Theorem fvelrnb 6945

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 6944	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2851	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6898	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2853	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3164	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2769	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2772	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 290	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3191	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3647	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146  {cab 2743  ∃wrex 3091  Vcvv 3457  ran crn 5664   Fn wfn 6535  ‘cfv 6540

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6496  df-fun 6542  df-fn 6543  df-fv 6548

This theorem is used by:  foelcdmi  6946  chfnrn  7048  rexrn  7086  ralrn  7087  elrnrexdmb  7089  ffnfv  7118  elunirn  7254  isoini  7345  canth  7373  mptcnfimad  7989  reldm  8047  seqomlem2  8444  fipreima  9322  ordiso2  9484  inf0  9597  inf3lem6  9609  noinfep  9636  cantnflem4  9668  infenaleph  10091  isinfcard  10092  dfac5  10128  ackbij1  10236  sornom  10276  fin23lem16  10334  fin23lem21  10338  isf32lem2  10353  fin1a2lem5  10403  itunitc  10420  axdc3lem2  10450  zorn2lem4  10498  cfpwsdom  10584  peano2nn  12260  uzn0  12895  om2uzrani  14006  uzrdgfni  14012  uzin2  15420  unbenlem  16990  vdwlem6  17068  0ram  17102  chnso  18702  imasmnd2  18869  imasgrp2  19165  cycsubmel  19315  ghmqusker  19401  pmtrfrn  19572  pgpssslw  19728  efgsfo  19853  efgrelexlemb  19864  gexex  19967  imasrng  20299  imasring  20458  lindfrn  22021  mpfind  22316  mpfpf1  22561  pf1mpf  22562  2ndcomap  23666  kgenidm  23755  kqreglem1  23949  zfbas  24104  rnelfmlem  24160  rnelfm  24161  fmfnfmlem2  24163  ovolctb  25700  ovolicc2  25732  mbfinf  25875  dvivth  26220  dvne0  26221  aannenlem3  26544  reeff1o  26661  oniso  28515  noseqp1  28535  noseqrdgfn  28550  bdayn0sf1o  28614  dfnns2  28616  uhgr2edg  29616  ushgredgedg  29637  ushgredgedgloop  29639  2pthon3v  30359  rnbra  32530  cnvbraval  32533  pjssdif1i  32598  dfpjop  32605  elpjrn  32613  foresf1o  32921  ressupprn  33106  fsumiunle  33243  mgcf1o  33387  imaslmod  33737  dimkerim  34081  rhmpreimacn  34339  esumfsup  34524  esumiun  34548  onvf1odlem4  35647  msrid  36074  tailfb  36945  indexdom  38443  cdleme50rnlem  41376  diaelrnN  41877  diaintclN  41890  cdlemm10N  41950  dibintclN  41999  dihglb2  42174  dihintcl  42176  lcfrlem9  42382  mapd1o  42480  hdmaprnlem11N  42692  hgmaprnlem4N  42731  sticksstones1  42971  aks6d1c6isolem1  42999  aks6d1c6isolem2  43000  aks6d1c6lem5  43002  unitscyglem1  43020  nacsfix  43501  orbitcl  45724  fvelrnbf  45796  cncmpmax  45810  climinf2lem  46478  stoweidlem27  46799  stoweidlem31  46803  stoweidlem48  46820  stoweidlem59  46831  stirlinglem13  46858  fourierdlem12  46891  fourierdlem41  46920  fourierdlem42  46921  fourierdlem46  46924  fourierdlem48  46926  fourierdlem49  46927  fourierdlem70  46948  fourierdlem71  46949  fourierdlem74  46952  fourierdlem75  46953  fourierdlem102  46980  fourierdlem103  46981  fourierdlem104  46982  fourierdlem114  46992  sge0tsms  47152  sge0sup  47163  sge0le  47179  sge0isum  47199  sge0seq  47218  nnfoctbdjlem  47227  meadjiunlem  47237  fcoresf1  47864  iccpartrn  48237  iccpartnel  48245  fmtnorn  48344  isubgredg  48689  gricushgr  48740