Theorem elrnmpti 5941

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ↦ cmpt 5186  ran crn 5649

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 2213  ax-ext 2732  ax-sep 5249  ax-pr 5391

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 2564  df-eu 2594  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-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-cnv 5656  df-dm 5658  df-rn 5659

This theorem is used by:  fliftel  7306  oarec  8549  unfilem1  9275  swrdrn3  14755  elrest  17545  psgneldm2  19665  psgnfitr  19678  iscyggen2  20042  iscyg3  20047  cycsubgcyg  20062  eldprd  20167  leordtval2  23477  iocpnfordt  23480  icomnfordt  23481  lecldbas  23484  tsmsxplem1  24419  minveclem2  25694  lhop2  26282  taylthlem2  26650  fsumvma  27489  dchrptlem2  27541  2sqlem1  27693  dchrisum0fno1  27787  minvecolem2  31396  domnprodeq0  33759  nsgqusf1olem1  33883  nsgqusf1olem3  33885  rspectopn  34418  zarclsun  34421  zarcls  34425  gsumesum  34610  esumlub  34611  esumcst  34614  esumpcvgval  34629  esumgect  34641  esum2d  34644  sigapildsys  34714  sxbrsigalem2  34838  omssubaddlem  34851  omssubadd  34852  eulerpartgbij  34924  actfunsnf1o  35153  actfunsnrndisj  35154  reprsuc  35164  breprexplema  35179  bnj1366  35379  msubco  36211  msubvrs  36240  mh-inf3sn  37246  fin2so  38444  poimirlem17  38469  poimirlem20  38472  cntotbnd  38644  islsat  39962