Theorem fvelrnb 6728

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 6727	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2900	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6685	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2902	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 235	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3284	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2827	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2830	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	syl6bb 289	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3299	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3676	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	syl6bb 289	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {cab 2801  ∃wrex 3141  Vcvv 3496  ran crn 5558   Fn wfn 6352  ‘cfv 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-iota 6316  df-fun 6359  df-fn 6360  df-fv 6365

This theorem is referenced by:  foelrni  6729  chfnrn  6821  rexrn  6855  ralrn  6856  elrnrexdmb  6858  ffnfv  6884  elunirn  7012  isoini  7093  canth  7113  reldm  7745  seqomlem2  8089  fipreima  8832  ordiso2  8981  inf0  9086  inf3lem6  9098  noinfep  9125  cantnflem4  9157  infenaleph  9519  isinfcard  9520  dfac5  9556  ackbij1  9662  sornom  9701  fin23lem16  9759  fin23lem21  9763  isf32lem2  9778  fin1a2lem5  9828  itunitc  9845  axdc3lem2  9875  zorn2lem4  9923  cfpwsdom  10008  peano2nn  11652  uzn0  12263  om2uzrani  13323  uzrdgfni  13329  uzin2  14706  unbenlem  16246  vdwlem6  16324  0ram  16358  imasmnd2  17950  imasgrp2  18216  cycsubmel  18345  pmtrfrn  18588  pgpssslw  18741  efgsfo  18867  efgrelexlemb  18878  gexex  18975  imasring  19371  mpfind  20322  mpfpf1  20516  pf1mpf  20517  lindfrn  20967  2ndcomap  22068  kgenidm  22157  kqreglem1  22351  zfbas  22506  rnelfmlem  22562  rnelfm  22563  fmfnfmlem2  22565  ovolctb  24093  ovolicc2  24125  mbfinf  24268  dvivth  24609  dvne0  24610  aannenlem3  24921  reeff1o  25037  uhgr2edg  26992  ushgredgedg  27013  ushgredgedgloop  27015  2pthon3v  27724  rnbra  29886  cnvbraval  29889  pjssdif1i  29954  dfpjop  29961  elpjrn  29969  foresf1o  30267  fsumiunle  30547  imaslmod  30924  dimkerim  31025  esumfsup  31331  esumiun  31355  msrid  32794  tailfb  33727  indexdom  35011  cdleme50rnlem  37682  diaelrnN  38183  diaintclN  38196  cdlemm10N  38256  dibintclN  38305  dihglb2  38480  dihintcl  38482  lcfrlem9  38688  mapd1o  38786  hdmaprnlem11N  38998  hgmaprnlem4N  39037  nacsfix  39316  fvelrnbf  41282  cncmpmax  41296  climinf2lem  41994  stoweidlem27  42319  stoweidlem31  42323  stoweidlem48  42340  stoweidlem59  42351  stirlinglem13  42378  fourierdlem12  42411  fourierdlem41  42440  fourierdlem42  42441  fourierdlem46  42444  fourierdlem48  42446  fourierdlem49  42447  fourierdlem70  42468  fourierdlem71  42469  fourierdlem74  42472  fourierdlem75  42473  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem114  42512  sge0tsms  42669  sge0sup  42680  sge0le  42696  sge0isum  42716  sge0seq  42735  nnfoctbdjlem  42744  meadjiunlem  42754  iccpartrn  43597  iccpartnel  43605  fmtnorn  43703  isomushgr  43998