Theorem elrnmpti 5917

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061  Vcvv 3429   ↦ cmpt 5166  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  fliftel  7264  oarec  8497  unfilem1  9215  elrest  17390  psgneldm2  19479  psgnfitr  19492  iscyggen2  19856  iscyg3  19861  cycsubgcyg  19876  eldprd  19981  leordtval2  23177  iocpnfordt  23180  icomnfordt  23181  lecldbas  23184  tsmsxplem1  24118  minveclem2  25393  lhop2  25982  taylthlem2  26339  fsumvma  27176  dchrptlem2  27228  2sqlem1  27380  dchrisum0fno1  27474  minvecolem2  30946  swrdrn3  33015  domnprodeq0  33337  nsgqusf1olem1  33473  nsgqusf1olem3  33475  rspectopn  34011  zarclsun  34014  zarcls  34018  gsumesum  34203  esumlub  34204  esumcst  34207  esumpcvgval  34222  esumgect  34234  esum2d  34237  sigapildsys  34306  sxbrsigalem2  34430  omssubaddlem  34443  omssubadd  34444  eulerpartgbij  34516  actfunsnf1o  34748  actfunsnrndisj  34749  reprsuc  34759  breprexplema  34774  bnj1366  34971  msubco  35713  msubvrs  35742  mh-inf3sn  36724  fin2so  37928  poimirlem17  37958  poimirlem20  37961  cntotbnd  38117  islsat  39437