Theorem fvelrnb 6950

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 6949	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2846	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6903	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2848	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3159	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2764	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2767	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 290	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3186	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3639	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {cab 2738  ∃wrex 3086  Vcvv 3450  ran crn 5652   Fn wfn 6538  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6497  df-fun 6545  df-fn 6546  df-fv 6551

This theorem is used by:  foelcdmi  6951  chfnrn  7053  rexrn  7092  ralrn  7093  elrnrexdmb  7095  ffnfv  7124  elunirn  7259  isoini  7350  canth  7378  mptcnfimad  8002  reldm  8059  seqomlem2  8468  fipreima  9354  ordiso2  9516  inf0  9629  inf3lem6  9641  noinfep  9668  cantnflem4  9700  infenaleph  10177  isinfcard  10178  dfac5  10214  ackbij1  10322  sornom  10362  fin23lem16  10420  fin23lem21  10424  isf32lem2  10439  fin1a2lem5  10489  itunitc  10506  axdc3lem2  10536  zorn2lem4  10584  cfpwsdom  10676  peano2nn  12354  uzn0  12989  om2uzrani  14102  uzrdgfni  14108  uzin2  15521  unbenlem  17095  vdwlem6  17173  0ram  17207  chnso  18807  imasmgm2  18872  imasmnd2  18977  imasgrp2  19274  cycsubmel  19424  ghmqusker  19510  pmtrfrn  19681  pgpssslw  19837  efgsfo  19962  efgrelexlemb  19973  gexex  20076  imasrng  20408  imasring  20569  lindfrn  22136  mpfind  22433  mpfpf1  22678  pf1mpf  22679  2ndcomap  23786  kgenidm  23875  kqreglem1  24069  zfbas  24224  rnelfmlem  24280  rnelfm  24281  fmfnfmlem2  24283  ovolctb  25820  ovolicc2  25852  mbfinf  25995  dvivth  26339  dvne0  26340  plyconz  26640  aannenlem3  26666  reeff1o  26783  oniso  28666  noseqp1  28686  noseqrdgfn  28701  bdayn0sf1o  28765  dfnns2  28767  uhgr2edg  29798  ushgredgedg  29819  ushgredgedgloop  29821  2pthon3v  30541  rnbra  32718  cnvbraval  32721  pjssdif1i  32786  dfpjop  32793  elpjrn  32801  foresf1o  33151  ressupprn  33334  fsumiunle  33470  mgcf1o  33614  imaslmod  33964  dimkerim  34309  rhmpreimacn  34567  esumfsup  34752  esumiun  34776  onvf1odlem4  35957  msrid  36400  tailfb  37261  indexdom  38777  cdleme50rnlem  41710  diaelrnN  42211  diaintclN  42224  cdlemm10N  42284  dibintclN  42333  dihglb2  42508  dihintcl  42510  lcfrlem9  42716  mapd1o  42814  hdmaprnlem11N  43026  hgmaprnlem4N  43065  sticksstones1  43305  aks6d1c6isolem1  43333  aks6d1c6isolem2  43334  aks6d1c6lem5  43336  unitscyglem1  43354  nacsfix  43832  orbitcl  46055  fvelrnbf  46143  cncmpmax  46157  climinf2lem  46824  stoweidlem27  47145  stoweidlem31  47149  stoweidlem48  47166  stoweidlem59  47177  stirlinglem13  47204  fourierdlem12  47237  fourierdlem41  47266  fourierdlem42  47267  fourierdlem46  47270  fourierdlem48  47272  fourierdlem49  47273  fourierdlem70  47294  fourierdlem71  47295  fourierdlem74  47298  fourierdlem75  47299  fourierdlem102  47326  fourierdlem103  47327  fourierdlem104  47328  fourierdlem114  47338  sge0tsms  47498  sge0sup  47509  sge0le  47525  sge0isum  47545  sge0seq  47564  nnfoctbdjlem  47573  meadjiunlem  47583  fcoresf1  48247  iccpartrn  48620  iccpartnel  48628  fmtnorn  48727  isubgredg  49072  gricushgr  49123