Theorem elrnmpti 5904

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  Vcvv 3436   ↦ cmpt 5173  ran crn 5620

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  fliftel  7246  oarec  8480  unfilem1  9194  elrest  17331  psgneldm2  19383  psgnfitr  19396  iscyggen2  19760  iscyg3  19765  cycsubgcyg  19780  eldprd  19885  leordtval2  23097  iocpnfordt  23100  icomnfordt  23101  lecldbas  23104  tsmsxplem1  24038  minveclem2  25324  lhop2  25918  taylthlem2  26280  taylthlem2OLD  26281  fsumvma  27122  dchrptlem2  27174  2sqlem1  27326  dchrisum0fno1  27420  minvecolem2  30819  swrdrn3  32898  nsgqusf1olem1  33351  nsgqusf1olem3  33353  rspectopn  33840  zarclsun  33843  zarcls  33847  gsumesum  34032  esumlub  34033  esumcst  34036  esumpcvgval  34051  esumgect  34063  esum2d  34066  sigapildsys  34135  sxbrsigalem2  34260  omssubaddlem  34273  omssubadd  34274  eulerpartgbij  34346  actfunsnf1o  34578  actfunsnrndisj  34579  reprsuc  34589  breprexplema  34604  bnj1366  34802  msubco  35514  msubvrs  35543  fin2so  37597  poimirlem17  37627  poimirlem20  37630  cntotbnd  37786  islsat  38980