Theorem fvelrnb 6968

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 6967	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2826	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6918	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2828	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 233	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3150	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2740	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2743	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 287	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3178	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3685	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 287	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  {cab 2713  ∃wrex 3069  Vcvv 3479  ran crn 5685   Fn wfn 6555  ‘cfv 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-iota 6513  df-fun 6562  df-fn 6563  df-fv 6568

This theorem is referenced by:  foelcdmi  6969  chfnrn  7068  rexrn  7106  ralrn  7107  elrnrexdmb  7109  ffnfv  7138  elunirn  7272  isoini  7359  canth  7386  mptcnfimad  8012  reldm  8070  seqomlem2  8492  fipreima  9399  ordiso2  9556  inf0  9662  inf3lem6  9674  noinfep  9701  cantnflem4  9733  infenaleph  10132  isinfcard  10133  dfac5  10170  ackbij1  10278  sornom  10318  fin23lem16  10376  fin23lem21  10380  isf32lem2  10395  fin1a2lem5  10445  itunitc  10462  axdc3lem2  10492  zorn2lem4  10540  cfpwsdom  10625  peano2nn  12279  uzn0  12896  om2uzrani  13994  uzrdgfni  14000  uzin2  15384  unbenlem  16947  vdwlem6  17025  0ram  17059  imasmnd2  18788  imasgrp2  19074  cycsubmel  19219  ghmqusker  19306  pmtrfrn  19477  pgpssslw  19633  efgsfo  19758  efgrelexlemb  19769  gexex  19872  imasrng  20175  imasring  20328  lindfrn  21842  mpfind  22132  mpfpf1  22356  pf1mpf  22357  2ndcomap  23467  kgenidm  23556  kqreglem1  23750  zfbas  23905  rnelfmlem  23961  rnelfm  23962  fmfnfmlem2  23964  ovolctb  25526  ovolicc2  25558  mbfinf  25701  dvivth  26050  dvne0  26051  aannenlem3  26373  reeff1o  26492  noseqp1  28298  noseqrdgfn  28313  dfnns2  28363  uhgr2edg  29226  ushgredgedg  29247  ushgredgedgloop  29249  2pthon3v  29964  rnbra  32127  cnvbraval  32130  pjssdif1i  32195  dfpjop  32202  elpjrn  32210  foresf1o  32524  ressupprn  32700  fsumiunle  32832  mgcf1o  32994  chnso  33005  imaslmod  33382  dimkerim  33679  rhmpreimacn  33885  esumfsup  34072  esumiun  34096  msrid  35551  tailfb  36379  indexdom  37742  cdleme50rnlem  40547  diaelrnN  41048  diaintclN  41061  cdlemm10N  41121  dibintclN  41170  dihglb2  41345  dihintcl  41347  lcfrlem9  41553  mapd1o  41651  hdmaprnlem11N  41863  hgmaprnlem4N  41902  sticksstones1  42148  aks6d1c6isolem1  42176  aks6d1c6isolem2  42177  aks6d1c6lem5  42179  unitscyglem1  42197  nacsfix  42728  fvelrnbf  45028  cncmpmax  45042  climinf2lem  45726  stoweidlem27  46047  stoweidlem31  46051  stoweidlem48  46068  stoweidlem59  46079  stirlinglem13  46106  fourierdlem12  46139  fourierdlem41  46168  fourierdlem42  46169  fourierdlem46  46172  fourierdlem48  46174  fourierdlem49  46175  fourierdlem70  46196  fourierdlem71  46197  fourierdlem74  46200  fourierdlem75  46201  fourierdlem102  46228  fourierdlem103  46229  fourierdlem104  46230  fourierdlem114  46240  sge0tsms  46400  sge0sup  46411  sge0le  46427  sge0isum  46447  sge0seq  46466  nnfoctbdjlem  46475  meadjiunlem  46485  fcoresf1  47086  iccpartrn  47422  iccpartnel  47430  fmtnorn  47526  isubgredg  47857  gricushgr  47891