Theorem elrnmpti 5959

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070  Vcvv 3474   ↦ cmpt 5231  ran crn 5677

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-cnv 5684  df-dm 5686  df-rn 5687

This theorem is referenced by:  fliftel  7305  oarec  8561  unfilem1  9309  pwfilemOLD  9345  elrest  17372  psgneldm2  19371  psgnfitr  19384  iscyggen2  19748  iscyg3  19753  cycsubgcyg  19768  eldprd  19873  leordtval2  22715  iocpnfordt  22718  icomnfordt  22719  lecldbas  22722  tsmsxplem1  23656  minveclem2  24942  lhop2  25531  taylthlem2  25885  fsumvma  26713  dchrptlem2  26765  2sqlem1  26917  dchrisum0fno1  27011  minvecolem2  30123  swrdrn3  32114  nsgqusf1olem1  32519  nsgqusf1olem3  32521  rspectopn  32842  zarclsun  32845  zarcls  32849  gsumesum  33052  esumlub  33053  esumcst  33056  esumpcvgval  33071  esumgect  33083  esum2d  33086  sigapildsys  33155  sxbrsigalem2  33280  omssubaddlem  33293  omssubadd  33294  eulerpartgbij  33366  actfunsnf1o  33611  actfunsnrndisj  33612  reprsuc  33622  breprexplema  33637  bnj1366  33835  msubco  34517  msubvrs  34546  fin2so  36470  poimirlem17  36500  poimirlem20  36503  cntotbnd  36659  islsat  37856