Theorem elrnmpti 5909

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3049  ∃wrex 3058  Vcvv 3438   ↦ cmpt 5177  ran crn 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-mpt 5178  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  fliftel  7253  oarec  8487  unfilem1  9203  elrest  17345  psgneldm2  19431  psgnfitr  19444  iscyggen2  19808  iscyg3  19813  cycsubgcyg  19828  eldprd  19933  leordtval2  23154  iocpnfordt  23157  icomnfordt  23158  lecldbas  23161  tsmsxplem1  24095  minveclem2  25380  lhop2  25974  taylthlem2  26336  taylthlem2OLD  26337  fsumvma  27178  dchrptlem2  27230  2sqlem1  27382  dchrisum0fno1  27476  minvecolem2  30899  swrdrn3  32986  domnprodeq0  33307  nsgqusf1olem1  33443  nsgqusf1olem3  33445  rspectopn  33973  zarclsun  33976  zarcls  33980  gsumesum  34165  esumlub  34166  esumcst  34169  esumpcvgval  34184  esumgect  34196  esum2d  34199  sigapildsys  34268  sxbrsigalem2  34392  omssubaddlem  34405  omssubadd  34406  eulerpartgbij  34478  actfunsnf1o  34710  actfunsnrndisj  34711  reprsuc  34721  breprexplema  34736  bnj1366  34934  msubco  35674  msubvrs  35703  fin2so  37747  poimirlem17  37777  poimirlem20  37780  cntotbnd  37936  islsat  39190