Theorem elrnmpti 5957

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071  Vcvv 3475   ↦ cmpt 5230  ran crn 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-mpt 5231  df-cnv 5683  df-dm 5685  df-rn 5686

This theorem is referenced by:  fliftel  7301  oarec  8558  unfilem1  9306  pwfilemOLD  9342  elrest  17369  psgneldm2  19365  psgnfitr  19378  iscyggen2  19741  iscyg3  19746  cycsubgcyg  19761  eldprd  19866  leordtval2  22698  iocpnfordt  22701  icomnfordt  22702  lecldbas  22705  tsmsxplem1  23639  minveclem2  24925  lhop2  25514  taylthlem2  25868  fsumvma  26696  dchrptlem2  26748  2sqlem1  26900  dchrisum0fno1  26994  minvecolem2  30106  swrdrn3  32097  nsgqusf1olem1  32487  nsgqusf1olem3  32489  rspectopn  32785  zarclsun  32788  zarcls  32792  gsumesum  32995  esumlub  32996  esumcst  32999  esumpcvgval  33014  esumgect  33026  esum2d  33029  sigapildsys  33098  sxbrsigalem2  33223  omssubaddlem  33236  omssubadd  33237  eulerpartgbij  33309  actfunsnf1o  33554  actfunsnrndisj  33555  reprsuc  33565  breprexplema  33580  bnj1366  33778  msubco  34460  msubvrs  34489  fin2so  36413  poimirlem17  36443  poimirlem20  36446  cntotbnd  36602  islsat  37799