Theorem fvelrnb 6724

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 6723	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2818	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6681	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2820	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3191	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2742	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2745	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 290	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3206	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3578	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1542   ∈ wcel 2113  {cab 2716  ∃wrex 3054  Vcvv 3397  ran crn 5520   Fn wfn 6328  ‘cfv 6333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-v 3399  df-sbc 3680  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6291  df-fun 6335  df-fn 6336  df-fv 6341

This theorem is referenced by:  foelrni  6725  chfnrn  6820  rexrn  6857  ralrn  6858  elrnrexdmb  6860  ffnfv  6886  elunirn  7015  isoini  7098  canth  7118  reldm  7761  seqomlem2  8109  fipreima  8896  ordiso2  9045  inf0  9150  inf3lem6  9162  noinfep  9189  cantnflem4  9221  infenaleph  9584  isinfcard  9585  dfac5  9621  ackbij1  9731  sornom  9770  fin23lem16  9828  fin23lem21  9832  isf32lem2  9847  fin1a2lem5  9897  itunitc  9914  axdc3lem2  9944  zorn2lem4  9992  cfpwsdom  10077  peano2nn  11721  uzn0  12334  om2uzrani  13404  uzrdgfni  13410  uzin2  14787  unbenlem  16337  vdwlem6  16415  0ram  16449  imasmnd2  18057  imasgrp2  18325  cycsubmel  18454  pmtrfrn  18697  pgpssslw  18850  efgsfo  18976  efgrelexlemb  18987  gexex  19085  imasring  19484  lindfrn  20630  mpfind  20914  mpfpf1  21114  pf1mpf  21115  2ndcomap  22202  kgenidm  22291  kqreglem1  22485  zfbas  22640  rnelfmlem  22696  rnelfm  22697  fmfnfmlem2  22699  ovolctb  24235  ovolicc2  24267  mbfinf  24410  dvivth  24754  dvne0  24755  aannenlem3  25070  reeff1o  25186  uhgr2edg  27142  ushgredgedg  27163  ushgredgedgloop  27165  2pthon3v  27873  rnbra  30034  cnvbraval  30037  pjssdif1i  30102  dfpjop  30109  elpjrn  30117  foresf1o  30416  ressupprn  30591  fsumiunle  30710  mgcf1o  30850  imaslmod  31117  dimkerim  31272  rhmpreimacn  31399  esumfsup  31600  esumiun  31624  msrid  33070  tailfb  34196  indexdom  35504  cdleme50rnlem  38170  diaelrnN  38671  diaintclN  38684  cdlemm10N  38744  dibintclN  38793  dihglb2  38968  dihintcl  38970  lcfrlem9  39176  mapd1o  39274  hdmaprnlem11N  39486  hgmaprnlem4N  39525  sticksstones1  39697  nacsfix  40090  fvelrnbf  42083  cncmpmax  42097  climinf2lem  42773  stoweidlem27  43094  stoweidlem31  43098  stoweidlem48  43115  stoweidlem59  43126  stirlinglem13  43153  fourierdlem12  43186  fourierdlem41  43215  fourierdlem42  43216  fourierdlem46  43219  fourierdlem48  43221  fourierdlem49  43222  fourierdlem70  43243  fourierdlem71  43244  fourierdlem74  43247  fourierdlem75  43248  fourierdlem102  43275  fourierdlem103  43276  fourierdlem104  43277  fourierdlem114  43287  sge0tsms  43444  sge0sup  43455  sge0le  43471  sge0isum  43491  sge0seq  43510  nnfoctbdjlem  43519  meadjiunlem  43529  fcoresf1  44085  iccpartrn  44400  iccpartnel  44408  fmtnorn  44504  isomushgr  44796