Theorem fvelrnb 6976

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 6975	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2850	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6929	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2852	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3163	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2767	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2770	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 290	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3190	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3643	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {cab 2741  ∃wrex 3090  Vcvv 3454  ran crn 5659   Fn wfn 6561  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-iota 6520  df-fun 6568  df-fn 6569  df-fv 6574

This theorem is used by:  foelcdmi  6977  chfnrn  7079  rexrn  7119  ralrn  7120  elrnrexdmb  7122  ffnfv  7151  elunirn  7286  isoini  7377  canth  7405  mptcnfimad  8032  reldmOLD  8090  seqomlem2  8499  fipreima  9385  ordiso2  9546  inf0  9659  inf3lem6  9671  noinfep  9698  cantnflem4  9730  infenaleph  10209  isinfcard  10210  dfac5  10246  ackbij1  10354  sornom  10394  fin23lem16  10452  fin23lem21  10456  isf32lem2  10471  fin1a2lem5  10521  itunitc  10538  axdc3lem2  10568  zorn2lem4  10616  cfpwsdom  10708  peano2nn  12387  uzn0  13022  om2uzrani  14135  uzrdgfni  14141  uzin2  15556  unbenlem  17130  vdwlem6  17208  0ram  17242  chnso  18848  imasmgm2  18913  imasmnd2  19018  imasgrp2  19315  cycsubmel  19465  ghmqusker  19552  pmtrfrn  19723  pgpssslw  19879  efgsfo  20004  efgrelexlemb  20015  gexex  20118  imasrng  20450  imasring  20611  lindfrn  22182  mpfind  22479  mpfpf1  22724  pf1mpf  22725  2ndcomap  23832  kgenidm  23921  kqreglem1  24115  zfbas  24270  rnelfmlem  24326  rnelfm  24327  fmfnfmlem2  24329  ovolctb  25866  ovolicc2  25898  mbfinf  26041  dvivth  26385  dvne0  26386  plyconz  26686  aannenlem3  26714  reeff1o  26831  oniso  28714  noseqp1  28734  noseqrdgfn  28749  bdayn0sf1o  28813  dfnns2  28815  uhgr2edg  29846  ushgredgedg  29867  ushgredgedgloop  29869  2pthon3v  30589  rnbra  32766  cnvbraval  32769  pjssdif1i  32834  dfpjop  32841  elpjrn  32849  foresf1o  33199  ressupprn  33380  fsumiunle  33516  mgcf1o  33663  imaslmod  34018  dimkerim  34370  rhmpreimacn  34628  esumfsup  34813  esumiun  34837  onvf1odlem4  36075  msrid  36518  tailfb  37380  indexdom  38936  cdleme50rnlem  41867  diaelrnN  42368  diaintclN  42381  cdlemm10N  42441  dibintclN  42490  dihglb2  42665  dihintcl  42667  lcfrlem9  42873  mapd1o  42971  hdmaprnlem11N  43183  hgmaprnlem4N  43222  sticksstones1  43462  aks6d1c6isolem1  43490  aks6d1c6isolem2  43491  aks6d1c6lem5  43493  unitscyglem1  43511  nacsfix  43989  orbitcl  46211  fvelrnbf  46309  cncmpmax  46323  climinf2lem  46989  stoweidlem27  47310  stoweidlem31  47314  stoweidlem48  47331  stoweidlem59  47342  stirlinglem13  47369  fourierdlem12  47402  fourierdlem41  47431  fourierdlem42  47432  fourierdlem46  47435  fourierdlem48  47437  fourierdlem49  47438  fourierdlem70  47459  fourierdlem71  47460  fourierdlem74  47463  fourierdlem75  47464  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  sge0tsms  47663  sge0sup  47674  sge0le  47690  sge0isum  47710  sge0seq  47729  nnfoctbdjlem  47738  meadjiunlem  47748  fcoresf1  48412  iccpartrn  48785  iccpartnel  48793  fmtnorn  48892  isubgredg  49237  gricushgr  49288