Theorem fvelrnb 6941

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 6940	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2849	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6894	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2851	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3162	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2767	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2770	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 290	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3189	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3645	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  {cab 2741  ∃wrex 3089  Vcvv 3455  ran crn 5662   Fn wfn 6531  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fn 6539  df-fv 6544

This theorem is referenced by:  foelcdmi  6942  chfnrn  7044  rexrn  7082  ralrn  7083  elrnrexdmb  7085  ffnfv  7114  elunirn  7249  isoini  7336  canth  7364  mptcnfimad  7979  reldm  8037  seqomlem2  8434  fipreima  9311  ordiso2  9473  inf0  9586  inf3lem6  9598  noinfep  9625  cantnflem4  9657  infenaleph  10071  isinfcard  10072  dfac5  10108  ackbij1  10216  sornom  10256  fin23lem16  10314  fin23lem21  10318  isf32lem2  10333  fin1a2lem5  10383  itunitc  10400  axdc3lem2  10430  zorn2lem4  10478  cfpwsdom  10564  peano2nn  12240  uzn0  12874  om2uzrani  13984  uzrdgfni  13990  uzin2  15392  unbenlem  16963  vdwlem6  17041  0ram  17075  chnso  18675  imasmnd2  18827  imasgrp2  19116  cycsubmel  19266  ghmqusker  19352  pmtrfrn  19523  pgpssslw  19679  efgsfo  19804  efgrelexlemb  19815  gexex  19918  imasrng  20250  imasring  20408  lindfrn  21971  mpfind  22266  mpfpf1  22511  pf1mpf  22512  2ndcomap  23615  kgenidm  23704  kqreglem1  23898  zfbas  24053  rnelfmlem  24109  rnelfm  24110  fmfnfmlem2  24112  ovolctb  25649  ovolicc2  25681  mbfinf  25824  dvivth  26169  dvne0  26170  aannenlem3  26493  reeff1o  26610  oniso  28464  noseqp1  28484  noseqrdgfn  28499  bdayn0sf1o  28563  dfnns2  28565  uhgr2edg  29558  ushgredgedg  29579  ushgredgedgloop  29581  2pthon3v  30292  rnbra  32459  cnvbraval  32462  pjssdif1i  32527  dfpjop  32534  elpjrn  32542  foresf1o  32850  ressupprn  33035  fsumiunle  33173  mgcf1o  33323  imaslmod  33673  dimkerim  34017  rhmpreimacn  34275  esumfsup  34460  esumiun  34484  onvf1odlem4  35590  msrid  36037  tailfb  36888  indexdom  38385  cdleme50rnlem  41318  diaelrnN  41819  diaintclN  41832  cdlemm10N  41892  dibintclN  41941  dihglb2  42116  dihintcl  42118  lcfrlem9  42324  mapd1o  42422  hdmaprnlem11N  42634  hgmaprnlem4N  42673  sticksstones1  42913  aks6d1c6isolem1  42941  aks6d1c6isolem2  42942  aks6d1c6lem5  42944  unitscyglem1  42962  nacsfix  43443  orbitcl  45666  fvelrnbf  45738  cncmpmax  45752  climinf2lem  46420  stoweidlem27  46741  stoweidlem31  46745  stoweidlem48  46762  stoweidlem59  46773  stirlinglem13  46800  fourierdlem12  46833  fourierdlem41  46862  fourierdlem42  46863  fourierdlem46  46866  fourierdlem48  46868  fourierdlem49  46869  fourierdlem70  46890  fourierdlem71  46891  fourierdlem74  46894  fourierdlem75  46895  fourierdlem102  46922  fourierdlem103  46923  fourierdlem104  46924  fourierdlem114  46934  sge0tsms  47094  sge0sup  47105  sge0le  47121  sge0isum  47141  sge0seq  47160  nnfoctbdjlem  47169  meadjiunlem  47179  fcoresf1  47806  iccpartrn  48179  iccpartnel  48187  fmtnorn  48286  isubgredg  48631  gricushgr  48682