Theorem elrnmpti 5943

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ↦ cmpt 5185  ran crn 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-mpt 5186  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  fliftel  7317  oarec  8570  unfilem1  9297  swrdrn3  14802  elrest  17598  psgneldm2  19718  psgnfitr  19731  iscyggen2  20095  iscyg3  20100  cycsubgcyg  20115  eldprd  20220  leordtval2  23530  iocpnfordt  23533  icomnfordt  23534  lecldbas  23537  tsmsxplem1  24472  minveclem2  25747  lhop2  26335  taylthlem2  26701  fsumvma  27540  dchrptlem2  27592  2sqlem1  27744  dchrisum0fno1  27838  minvecolem2  31477  domnprodeq0  33840  nsgqusf1olem1  33964  nsgqusf1olem3  33966  rspectopn  34499  zarclsun  34502  zarcls  34506  gsumesum  34691  esumlub  34692  esumcst  34695  esumpcvgval  34710  esumgect  34722  esum2d  34725  sigapildsys  34795  sxbrsigalem2  34918  omssubaddlem  34931  omssubadd  34932  eulerpartgbij  35004  actfunsnf1o  35233  actfunsnrndisj  35234  reprsuc  35244  breprexplema  35259  bnj1366  35459  msubco  36296  msubvrs  36325  mh-inf3sn  37330  fin2so  38531  poimirlem17  38556  poimirlem20  38559  cntotbnd  38731  islsat  40049