Theorem fvelrnb 6903

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {cab 2707  ∃wrex 3053  Vcvv 3444  ran crn 5632   Fn wfn 6494  ‘cfv 6499

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6452  df-fun 6501  df-fn 6502  df-fv 6507

This theorem is referenced by:  foelcdmi  6904  chfnrn  7003  rexrn  7041  ralrn  7042  elrnrexdmb  7044  ffnfv  7073  elunirn  7207  isoini  7295  canth  7323  mptcnfimad  7944  reldm  8002  seqomlem2  8396  fipreima  9285  ordiso2  9444  inf0  9550  inf3lem6  9562  noinfep  9589  cantnflem4  9621  infenaleph  10020  isinfcard  10021  dfac5  10058  ackbij1  10166  sornom  10206  fin23lem16  10264  fin23lem21  10268  isf32lem2  10283  fin1a2lem5  10333  itunitc  10350  axdc3lem2  10380  zorn2lem4  10428  cfpwsdom  10513  peano2nn  12174  uzn0  12786  om2uzrani  13893  uzrdgfni  13899  uzin2  15287  unbenlem  16855  vdwlem6  16933  0ram  16967  imasmnd2  18677  imasgrp2  18963  cycsubmel  19108  ghmqusker  19195  pmtrfrn  19364  pgpssslw  19520  efgsfo  19645  efgrelexlemb  19656  gexex  19759  imasrng  20062  imasring  20215  lindfrn  21706  mpfind  21990  mpfpf1  22214  pf1mpf  22215  2ndcomap  23321  kgenidm  23410  kqreglem1  23604  zfbas  23759  rnelfmlem  23815  rnelfm  23816  fmfnfmlem2  23818  ovolctb  25367  ovolicc2  25399  mbfinf  25542  dvivth  25891  dvne0  25892  aannenlem3  26214  reeff1o  26333  onsiso  28145  noseqp1  28161  noseqrdgfn  28176  bdayn0sf1o  28235  dfnns2  28237  uhgr2edg  29111  ushgredgedg  29132  ushgredgedgloop  29134  2pthon3v  29846  rnbra  32009  cnvbraval  32012  pjssdif1i  32077  dfpjop  32084  elpjrn  32092  foresf1o  32406  ressupprn  32586  fsumiunle  32727  mgcf1o  32902  chnso  32913  imaslmod  33297  dimkerim  33596  rhmpreimacn  33848  esumfsup  34033  esumiun  34057  onvf1odlem4  35066  msrid  35505  tailfb  36338  indexdom  37701  cdleme50rnlem  40511  diaelrnN  41012  diaintclN  41025  cdlemm10N  41085  dibintclN  41134  dihglb2  41309  dihintcl  41311  lcfrlem9  41517  mapd1o  41615  hdmaprnlem11N  41827  hgmaprnlem4N  41866  sticksstones1  42107  aks6d1c6isolem1  42135  aks6d1c6isolem2  42136  aks6d1c6lem5  42138  unitscyglem1  42156  nacsfix  42673  orbitcl  44920  fvelrnbf  44985  cncmpmax  44999  climinf2lem  45677  stoweidlem27  45998  stoweidlem31  46002  stoweidlem48  46019  stoweidlem59  46030  stirlinglem13  46057  fourierdlem12  46090  fourierdlem41  46119  fourierdlem42  46120  fourierdlem46  46123  fourierdlem48  46125  fourierdlem49  46126  fourierdlem70  46147  fourierdlem71  46148  fourierdlem74  46151  fourierdlem75  46152  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem114  46191  sge0tsms  46351  sge0sup  46362  sge0le  46378  sge0isum  46398  sge0seq  46417  nnfoctbdjlem  46426  meadjiunlem  46436  fcoresf1  47043  iccpartrn  47404  iccpartnel  47412  fmtnorn  47508  isubgredg  47839  gricushgr  47890