Theorem elrnmpti 5950

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088  Vcvv 3453   ↦ cmpt 5190  ran crn 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-mpt 5191  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is used by:  fliftel  7313  oarec  8552  unfilem1  9278  swrdrn3  14724  elrest  17516  psgneldm2  19632  psgnfitr  19645  iscyggen2  20009  iscyg3  20014  cycsubgcyg  20029  eldprd  20134  leordtval2  23438  iocpnfordt  23441  icomnfordt  23442  lecldbas  23445  tsmsxplem1  24380  minveclem2  25655  lhop2  26244  taylthlem2  26607  fsumvma  27447  dchrptlem2  27499  2sqlem1  27651  dchrisum0fno1  27745  minvecolem2  31342  domnprodeq0  33706  nsgqusf1olem1  33829  nsgqusf1olem3  33831  rspectopn  34364  zarclsun  34367  zarcls  34371  gsumesum  34556  esumlub  34557  esumcst  34560  esumpcvgval  34575  esumgect  34587  esum2d  34590  sigapildsys  34660  sxbrsigalem2  34784  omssubaddlem  34797  omssubadd  34798  eulerpartgbij  34870  actfunsnf1o  35099  actfunsnrndisj  35100  reprsuc  35110  breprexplema  35125  bnj1366  35325  msubco  36097  msubvrs  36126  mh-inf3sn  37148  fin2so  38348  poimirlem17  38373  poimirlem20  38376  cntotbnd  38533  islsat  39851