Theorem elrnmpti 5796

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

Syntax hints:   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ↦ cmpt 5110  ran crn 5520

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-mpt 5111  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  fliftel  7041  oarec  8171  unfilem1  8766  pwfilem  8802  elrest  16693  psgneldm2  18624  psgnfitr  18637  iscyggen2  18993  iscyg3  18998  cycsubgcyg  19014  eldprd  19119  leordtval2  21817  iocpnfordt  21820  icomnfordt  21821  lecldbas  21824  tsmsxplem1  22758  minveclem2  24030  lhop2  24618  taylthlem2  24969  fsumvma  25797  dchrptlem2  25849  2sqlem1  26001  dchrisum0fno1  26095  minvecolem2  28658  swrdrn3  30655  rspectopn  31220  zarclsun  31223  zarcls  31227  gsumesum  31428  esumlub  31429  esumcst  31432  esumpcvgval  31447  esumgect  31459  esum2d  31462  sigapildsys  31531  sxbrsigalem2  31654  omssubaddlem  31667  omssubadd  31668  eulerpartgbij  31740  actfunsnf1o  31985  actfunsnrndisj  31986  reprsuc  31996  breprexplema  32011  bnj1366  32211  msubco  32891  msubvrs  32920  fin2so  35044  poimirlem17  35074  poimirlem20  35077  cntotbnd  35234  islsat  36287