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 3084	. 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 2147  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ↦ cmpt 5189  ran crn 5656

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-mpt 5190  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  fliftel  7337  reldm  8076  oarec  8595  unfilem1  9322  swrdrn3  14827  elrest  17624  psgneldm2  19745  psgnfitr  19758  iscyggen2  20122  iscyg3  20127  cycsubgcyg  20142  eldprd  20247  leordtval2  23557  iocpnfordt  23560  icomnfordt  23561  lecldbas  23564  tsmsxplem1  24499  minveclem2  25774  lhop2  26362  taylthlem2  26728  fsumvma  27567  dchrptlem2  27619  2sqlem1  27771  dchrisum0fno1  27865  minvecolem2  31504  domnprodeq0  33907  nsgqusf1olem1  34031  nsgqusf1olem3  34033  rspectopn  34566  zarclsun  34569  zarcls  34573  gsumesum  34758  esumlub  34759  esumcst  34762  esumpcvgval  34777  esumgect  34789  esum2d  34792  sigapildsys  34862  sxbrsigalem2  34985  omssubaddlem  34998  omssubadd  34999  eulerpartgbij  35071  actfunsnf1o  35300  actfunsnrndisj  35301  reprsuc  35311  breprexplema  35326  bnj1366  35526  msubco  36462  msubvrs  36491  mh-inf3sn  37507  fin2so  38721  poimirlem17  38746  poimirlem20  38749  cntotbnd  38921  islsat  40239