Theorem fvelrnb 6883

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 6882	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2814	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6835	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2816	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3126	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2733	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2736	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3153	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3642	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  ∃wrex 3053  Vcvv 3436  ran crn 5620   Fn wfn 6477  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fn 6485  df-fv 6490

This theorem is referenced by:  foelcdmi  6884  chfnrn  6983  rexrn  7021  ralrn  7022  elrnrexdmb  7024  ffnfv  7053  elunirn  7187  isoini  7275  canth  7303  mptcnfimad  7921  reldm  7979  seqomlem2  8373  fipreima  9248  ordiso2  9407  inf0  9517  inf3lem6  9529  noinfep  9556  cantnflem4  9588  infenaleph  9985  isinfcard  9986  dfac5  10023  ackbij1  10131  sornom  10171  fin23lem16  10229  fin23lem21  10233  isf32lem2  10248  fin1a2lem5  10298  itunitc  10315  axdc3lem2  10345  zorn2lem4  10393  cfpwsdom  10478  peano2nn  12140  uzn0  12752  om2uzrani  13859  uzrdgfni  13865  uzin2  15252  unbenlem  16820  vdwlem6  16898  0ram  16932  imasmnd2  18648  imasgrp2  18934  cycsubmel  19079  ghmqusker  19166  pmtrfrn  19337  pgpssslw  19493  efgsfo  19618  efgrelexlemb  19629  gexex  19732  imasrng  20062  imasring  20215  lindfrn  21728  mpfind  22012  mpfpf1  22236  pf1mpf  22237  2ndcomap  23343  kgenidm  23432  kqreglem1  23626  zfbas  23781  rnelfmlem  23837  rnelfm  23838  fmfnfmlem2  23840  ovolctb  25389  ovolicc2  25421  mbfinf  25564  dvivth  25913  dvne0  25914  aannenlem3  26236  reeff1o  26355  onsiso  28174  noseqp1  28190  noseqrdgfn  28205  bdayn0sf1o  28264  dfnns2  28266  uhgr2edg  29153  ushgredgedg  29174  ushgredgedgloop  29176  2pthon3v  29888  rnbra  32051  cnvbraval  32054  pjssdif1i  32119  dfpjop  32126  elpjrn  32134  foresf1o  32448  ressupprn  32632  fsumiunle  32774  mgcf1o  32945  chnso  32956  imaslmod  33290  dimkerim  33594  rhmpreimacn  33852  esumfsup  34037  esumiun  34061  onvf1odlem4  35079  msrid  35518  tailfb  36351  indexdom  37714  cdleme50rnlem  40523  diaelrnN  41024  diaintclN  41037  cdlemm10N  41097  dibintclN  41146  dihglb2  41321  dihintcl  41323  lcfrlem9  41529  mapd1o  41627  hdmaprnlem11N  41839  hgmaprnlem4N  41878  sticksstones1  42119  aks6d1c6isolem1  42147  aks6d1c6isolem2  42148  aks6d1c6lem5  42150  unitscyglem1  42168  nacsfix  42685  orbitcl  44931  fvelrnbf  44996  cncmpmax  45010  climinf2lem  45687  stoweidlem27  46008  stoweidlem31  46012  stoweidlem48  46029  stoweidlem59  46040  stirlinglem13  46067  fourierdlem12  46100  fourierdlem41  46129  fourierdlem42  46130  fourierdlem46  46133  fourierdlem48  46135  fourierdlem49  46136  fourierdlem70  46157  fourierdlem71  46158  fourierdlem74  46161  fourierdlem75  46162  fourierdlem102  46189  fourierdlem103  46190  fourierdlem104  46191  fourierdlem114  46201  sge0tsms  46361  sge0sup  46372  sge0le  46388  sge0isum  46408  sge0seq  46427  nnfoctbdjlem  46436  meadjiunlem  46446  fcoresf1  47053  iccpartrn  47414  iccpartnel  47422  fmtnorn  47518  isubgredg  47850  gricushgr  47901