Theorem fvelrnb 6944

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 6943	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2821	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6894	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2823	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3138	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2740	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2743	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3165	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3670	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2714  ∃wrex 3061  Vcvv 3464  ran crn 5660   Fn wfn 6531  ‘cfv 6536

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6489  df-fun 6538  df-fn 6539  df-fv 6544

This theorem is referenced by:  foelcdmi  6945  chfnrn  7044  rexrn  7082  ralrn  7083  elrnrexdmb  7085  ffnfv  7114  elunirn  7248  isoini  7336  canth  7364  mptcnfimad  7990  reldm  8048  seqomlem2  8470  fipreima  9375  ordiso2  9534  inf0  9640  inf3lem6  9652  noinfep  9679  cantnflem4  9711  infenaleph  10110  isinfcard  10111  dfac5  10148  ackbij1  10256  sornom  10296  fin23lem16  10354  fin23lem21  10358  isf32lem2  10373  fin1a2lem5  10423  itunitc  10440  axdc3lem2  10470  zorn2lem4  10518  cfpwsdom  10603  peano2nn  12257  uzn0  12874  om2uzrani  13975  uzrdgfni  13981  uzin2  15368  unbenlem  16933  vdwlem6  17011  0ram  17045  imasmnd2  18757  imasgrp2  19043  cycsubmel  19188  ghmqusker  19275  pmtrfrn  19444  pgpssslw  19600  efgsfo  19725  efgrelexlemb  19736  gexex  19839  imasrng  20142  imasring  20295  lindfrn  21786  mpfind  22070  mpfpf1  22294  pf1mpf  22295  2ndcomap  23401  kgenidm  23490  kqreglem1  23684  zfbas  23839  rnelfmlem  23895  rnelfm  23896  fmfnfmlem2  23898  ovolctb  25448  ovolicc2  25480  mbfinf  25623  dvivth  25972  dvne0  25973  aannenlem3  26295  reeff1o  26414  onsiso  28226  noseqp1  28242  noseqrdgfn  28257  bdayn0sf1o  28316  dfnns2  28318  uhgr2edg  29192  ushgredgedg  29213  ushgredgedgloop  29215  2pthon3v  29930  rnbra  32093  cnvbraval  32096  pjssdif1i  32161  dfpjop  32168  elpjrn  32176  foresf1o  32490  ressupprn  32672  fsumiunle  32813  mgcf1o  32988  chnso  32999  imaslmod  33373  dimkerim  33672  rhmpreimacn  33921  esumfsup  34106  esumiun  34130  msrid  35572  tailfb  36400  indexdom  37763  cdleme50rnlem  40568  diaelrnN  41069  diaintclN  41082  cdlemm10N  41142  dibintclN  41191  dihglb2  41366  dihintcl  41368  lcfrlem9  41574  mapd1o  41672  hdmaprnlem11N  41884  hgmaprnlem4N  41923  sticksstones1  42164  aks6d1c6isolem1  42192  aks6d1c6isolem2  42193  aks6d1c6lem5  42195  unitscyglem1  42213  nacsfix  42710  orbitcl  44957  fvelrnbf  45022  cncmpmax  45036  climinf2lem  45715  stoweidlem27  46036  stoweidlem31  46040  stoweidlem48  46057  stoweidlem59  46068  stirlinglem13  46095  fourierdlem12  46128  fourierdlem41  46157  fourierdlem42  46158  fourierdlem46  46161  fourierdlem48  46163  fourierdlem49  46164  fourierdlem70  46185  fourierdlem71  46186  fourierdlem74  46189  fourierdlem75  46190  fourierdlem102  46217  fourierdlem103  46218  fourierdlem104  46219  fourierdlem114  46229  sge0tsms  46389  sge0sup  46400  sge0le  46416  sge0isum  46436  sge0seq  46455  nnfoctbdjlem  46464  meadjiunlem  46474  fcoresf1  47078  iccpartrn  47424  iccpartnel  47432  fmtnorn  47528  isubgredg  47859  gricushgr  47910