Theorem elrnmpti 5376

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

Syntax hints:   ↔ wb 196   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913  Vcvv 3200   ↦ cmpt 4729  ran crn 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-mpt 4730  df-cnv 5122  df-dm 5124  df-rn 5125

This theorem is referenced by:  fliftel  6559  oarec  7642  unfilem1  8224  pwfilem  8260  elrest  16088  psgneldm2  17924  psgnfitr  17937  iscyggen2  18283  iscyg3  18288  cycsubgcyg  18302  eldprd  18403  leordtval2  21016  iocpnfordt  21019  icomnfordt  21020  lecldbas  21023  tsmsxplem1  21956  minveclem2  23197  lhop2  23778  taylthlem2  24128  fsumvma  24938  dchrptlem2  24990  2sqlem1  25142  dchrisum0fno1  25200  minvecolem2  27731  gsumesum  30121  esumlub  30122  esumcst  30125  esumpcvgval  30140  esumgect  30152  esum2d  30155  sigapildsys  30225  sxbrsigalem2  30348  omssubaddlem  30361  omssubadd  30362  eulerpartgbij  30434  actfunsnf1o  30682  actfunsnrndisj  30683  reprsuc  30693  breprexplema  30708  bnj1366  30900  msubco  31428  msubvrs  31457  fin2so  33396  poimirlem17  33426  poimirlem20  33429  cntotbnd  33595  islsat  34278