Theorem fvelrnb 6938

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 6937	. . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})
2	1	eleq2d 2846	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}))
3		fvex 6891	. . . . 5 ⊢ (𝐹‘𝑥) ∈ V
4		eleq1 2848	. . . . 5 ⊢ ((𝐹‘𝑥) = 𝐵 → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V))
5	3, 4	mpbii 236	. . . 4 ⊢ ((𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
6	5	rexlimivw 3159	. . 3 ⊢ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)
7		eqeq1 2764	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥)))
8		eqcom 2767	. . . . 5 ⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)
9	7, 8	bitrdi 290	. . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵))
10	9	rexbidv 3186	. . 3 ⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
11	6, 10	elab3 3640	. 2 ⊢ (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)
12	2, 11	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {cab 2738  ∃wrex 3086  Vcvv 3450  ran crn 5656   Fn wfn 6528  ‘cfv 6533

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is used by:  foelcdmi  6939  chfnrn  7041  rexrn  7080  ralrn  7081  elrnrexdmb  7083  ffnfv  7112  elunirn  7248  isoini  7339  canth  7367  mptcnfimad  7983  reldm  8041  seqomlem2  8440  fipreima  9325  ordiso2  9487  inf0  9600  inf3lem6  9612  noinfep  9639  cantnflem4  9671  infenaleph  10094  isinfcard  10095  dfac5  10131  ackbij1  10239  sornom  10279  fin23lem16  10337  fin23lem21  10341  isf32lem2  10356  fin1a2lem5  10406  itunitc  10423  axdc3lem2  10453  zorn2lem4  10501  cfpwsdom  10593  peano2nn  12269  uzn0  12904  om2uzrani  14016  uzrdgfni  14022  uzin2  15432  unbenlem  17000  vdwlem6  17078  0ram  17112  chnso  18712  imasmgm2  18776  imasmnd2  18881  imasgrp2  19178  cycsubmel  19328  ghmqusker  19414  pmtrfrn  19585  pgpssslw  19741  efgsfo  19866  efgrelexlemb  19877  gexex  19980  imasrng  20312  imasring  20471  lindfrn  22034  mpfind  22331  mpfpf1  22576  pf1mpf  22577  2ndcomap  23684  kgenidm  23773  kqreglem1  23967  zfbas  24122  rnelfmlem  24178  rnelfm  24179  fmfnfmlem2  24181  ovolctb  25718  ovolicc2  25750  mbfinf  25893  dvivth  26237  dvne0  26238  plyconz  26540  aannenlem3  26566  reeff1o  26683  oniso  28536  noseqp1  28556  noseqrdgfn  28571  bdayn0sf1o  28635  dfnns2  28637  uhgr2edg  29668  ushgredgedg  29689  ushgredgedgloop  29691  2pthon3v  30411  rnbra  32588  cnvbraval  32591  pjssdif1i  32656  dfpjop  32663  elpjrn  32671  foresf1o  32979  ressupprn  33162  fsumiunle  33299  mgcf1o  33443  imaslmod  33793  dimkerim  34137  rhmpreimacn  34395  esumfsup  34580  esumiun  34604  onvf1odlem4  35703  msrid  36124  tailfb  36996  indexdom  38484  cdleme50rnlem  41417  diaelrnN  41918  diaintclN  41931  cdlemm10N  41991  dibintclN  42040  dihglb2  42215  dihintcl  42217  lcfrlem9  42423  mapd1o  42521  hdmaprnlem11N  42733  hgmaprnlem4N  42772  sticksstones1  43012  aks6d1c6isolem1  43040  aks6d1c6isolem2  43041  aks6d1c6lem5  43043  unitscyglem1  43061  nacsfix  43557  orbitcl  45780  fvelrnbf  45852  cncmpmax  45866  climinf2lem  46534  stoweidlem27  46855  stoweidlem31  46859  stoweidlem48  46876  stoweidlem59  46887  stirlinglem13  46914  fourierdlem12  46947  fourierdlem41  46976  fourierdlem42  46977  fourierdlem46  46980  fourierdlem48  46982  fourierdlem49  46983  fourierdlem70  47004  fourierdlem71  47005  fourierdlem74  47008  fourierdlem75  47009  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem114  47048  sge0tsms  47208  sge0sup  47219  sge0le  47235  sge0isum  47255  sge0seq  47274  nnfoctbdjlem  47283  meadjiunlem  47293  fcoresf1  47957  iccpartrn  48330  iccpartnel  48338  fmtnorn  48437  isubgredg  48782  gricushgr  48833