Theorem elrnmpti 5911

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

Syntax hints:   ↔ wb 208   = wceq 1548   ∈ wcel 2121  ∀wral 3055  ∃wrex 3065  Vcvv 3433   ↦ cmpt 5156  ran crn 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-mpt 5157  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  fliftel  7257  oarec  8491  unfilem1  9209  elrest  17385  psgneldm2  19474  psgnfitr  19487  iscyggen2  19851  iscyg3  19856  cycsubgcyg  19871  eldprd  19976  leordtval2  23199  iocpnfordt  23202  icomnfordt  23203  lecldbas  23206  tsmsxplem1  24140  minveclem2  25415  lhop2  26004  taylthlem2  26361  fsumvma  27198  dchrptlem2  27250  2sqlem1  27402  dchrisum0fno1  27496  minvecolem2  30968  swrdrn3  33038  domnprodeq0  33361  nsgqusf1olem1  33500  nsgqusf1olem3  33502  rspectopn  34063  zarclsun  34066  zarcls  34070  gsumesum  34255  esumlub  34256  esumcst  34259  esumpcvgval  34274  esumgect  34286  esum2d  34289  sigapildsys  34358  sxbrsigalem2  34482  omssubaddlem  34495  omssubadd  34496  eulerpartgbij  34568  actfunsnf1o  34800  actfunsnrndisj  34801  reprsuc  34811  breprexplema  34826  bnj1366  35026  msubco  35774  msubvrs  35803  mh-inf3sn  36785  fin2so  37989  poimirlem17  38019  poimirlem20  38022  cntotbnd  38178  islsat  39498