Theorem elrnmpti 5913

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 3056	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V
3		rnmpt.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
4	3	elrnmptg 5912	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵))
5	2, 4	ax-mp 5	1 ⊢ (𝐶 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝐶 = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  Vcvv 3430   ↦ cmpt 5167  ran crn 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-cnv 5634  df-dm 5636  df-rn 5637

This theorem is referenced by:  fliftel  7259  oarec  8492  unfilem1  9210  elrest  17385  psgneldm2  19474  psgnfitr  19487  iscyggen2  19851  iscyg3  19856  cycsubgcyg  19871  eldprd  19976  leordtval2  23191  iocpnfordt  23194  icomnfordt  23195  lecldbas  23198  tsmsxplem1  24132  minveclem2  25407  lhop2  25996  taylthlem2  26355  taylthlem2OLD  26356  fsumvma  27194  dchrptlem2  27246  2sqlem1  27398  dchrisum0fno1  27492  minvecolem2  30965  swrdrn3  33034  domnprodeq0  33356  nsgqusf1olem1  33492  nsgqusf1olem3  33494  rspectopn  34031  zarclsun  34034  zarcls  34038  gsumesum  34223  esumlub  34224  esumcst  34227  esumpcvgval  34242  esumgect  34254  esum2d  34257  sigapildsys  34326  sxbrsigalem2  34450  omssubaddlem  34463  omssubadd  34464  eulerpartgbij  34536  actfunsnf1o  34768  actfunsnrndisj  34769  reprsuc  34779  breprexplema  34794  bnj1366  34991  msubco  35733  msubvrs  35762  mh-inf3sn  36744  fin2so  37946  poimirlem17  37976  poimirlem20  37979  cntotbnd  38135  islsat  39455