Theorem elrnmpti 5973

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070  Vcvv 3480   ↦ cmpt 5225  ran crn 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-cnv 5693  df-dm 5695  df-rn 5696

This theorem is referenced by:  fliftel  7329  oarec  8600  unfilem1  9343  elrest  17472  psgneldm2  19522  psgnfitr  19535  iscyggen2  19899  iscyg3  19904  cycsubgcyg  19919  eldprd  20024  leordtval2  23220  iocpnfordt  23223  icomnfordt  23224  lecldbas  23227  tsmsxplem1  24161  minveclem2  25460  lhop2  26054  taylthlem2  26416  taylthlem2OLD  26417  fsumvma  27257  dchrptlem2  27309  2sqlem1  27461  dchrisum0fno1  27555  minvecolem2  30894  swrdrn3  32940  nsgqusf1olem1  33441  nsgqusf1olem3  33443  rspectopn  33866  zarclsun  33869  zarcls  33873  gsumesum  34060  esumlub  34061  esumcst  34064  esumpcvgval  34079  esumgect  34091  esum2d  34094  sigapildsys  34163  sxbrsigalem2  34288  omssubaddlem  34301  omssubadd  34302  eulerpartgbij  34374  actfunsnf1o  34619  actfunsnrndisj  34620  reprsuc  34630  breprexplema  34645  bnj1366  34843  msubco  35536  msubvrs  35565  fin2so  37614  poimirlem17  37644  poimirlem20  37647  cntotbnd  37803  islsat  38992