Theorem elrnmpti 5976

Description: Membership in the range of a function. (Contributed by NM, 30-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)

Hypotheses

Ref	Expression
rnmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
elrnmpti.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
elrnmpti	⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)

Distinct variable group:   𝑥,𝐶

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem elrnmpti

Step	Hyp	Ref	Expression
1		elrnmpti.2	. . 3 ⊢ 𝐵 ∈ V
2	1	rgenw 3063	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
3		rnmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	elrnmptg 5975	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
5	2, 4	ax-mp 5	1 ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068  Vcvv 3478   ↦ cmpt 5231  ran crn 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-mpt 5232  df-cnv 5697  df-dm 5699  df-rn 5700

This theorem is referenced by:  fliftel  7329  oarec  8599  unfilem1  9341  elrest  17474  psgneldm2  19537  psgnfitr  19550  iscyggen2  19914  iscyg3  19919  cycsubgcyg  19934  eldprd  20039  leordtval2  23236  iocpnfordt  23239  icomnfordt  23240  lecldbas  23243  tsmsxplem1  24177  minveclem2  25474  lhop2  26069  taylthlem2  26431  taylthlem2OLD  26432  fsumvma  27272  dchrptlem2  27324  2sqlem1  27476  dchrisum0fno1  27570  minvecolem2  30904  swrdrn3  32925  nsgqusf1olem1  33421  nsgqusf1olem3  33423  rspectopn  33828  zarclsun  33831  zarcls  33835  gsumesum  34040  esumlub  34041  esumcst  34044  esumpcvgval  34059  esumgect  34071  esum2d  34074  sigapildsys  34143  sxbrsigalem2  34268  omssubaddlem  34281  omssubadd  34282  eulerpartgbij  34354  actfunsnf1o  34598  actfunsnrndisj  34599  reprsuc  34609  breprexplema  34624  bnj1366  34822  msubco  35516  msubvrs  35545  fin2so  37594  poimirlem17  37624  poimirlem20  37627  cntotbnd  37783  islsat  38973