Theorem elrnmpti 5915

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  Vcvv 3444   ↦ cmpt 5183  ran crn 5632

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  fliftel  7266  oarec  8503  unfilem1  9230  elrest  17366  psgneldm2  19418  psgnfitr  19431  iscyggen2  19795  iscyg3  19800  cycsubgcyg  19815  eldprd  19920  leordtval2  23132  iocpnfordt  23135  icomnfordt  23136  lecldbas  23139  tsmsxplem1  24073  minveclem2  25359  lhop2  25953  taylthlem2  26315  taylthlem2OLD  26316  fsumvma  27157  dchrptlem2  27209  2sqlem1  27361  dchrisum0fno1  27455  minvecolem2  30854  swrdrn3  32927  nsgqusf1olem1  33377  nsgqusf1olem3  33379  rspectopn  33850  zarclsun  33853  zarcls  33857  gsumesum  34042  esumlub  34043  esumcst  34046  esumpcvgval  34061  esumgect  34073  esum2d  34076  sigapildsys  34145  sxbrsigalem2  34270  omssubaddlem  34283  omssubadd  34284  eulerpartgbij  34356  actfunsnf1o  34588  actfunsnrndisj  34589  reprsuc  34599  breprexplema  34614  bnj1366  34812  msubco  35511  msubvrs  35540  fin2so  37594  poimirlem17  37624  poimirlem20  37627  cntotbnd  37783  islsat  38977