Theorem elrnmpti 5912

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3061  Vcvv 3441   ↦ cmpt 5180  ran crn 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  fliftel  7257  oarec  8491  unfilem1  9209  elrest  17351  psgneldm2  19437  psgnfitr  19450  iscyggen2  19814  iscyg3  19819  cycsubgcyg  19834  eldprd  19939  leordtval2  23160  iocpnfordt  23163  icomnfordt  23164  lecldbas  23167  tsmsxplem1  24101  minveclem2  25386  lhop2  25980  taylthlem2  26342  taylthlem2OLD  26343  fsumvma  27184  dchrptlem2  27236  2sqlem1  27388  dchrisum0fno1  27482  minvecolem2  30954  swrdrn3  33039  domnprodeq0  33360  nsgqusf1olem1  33496  nsgqusf1olem3  33498  rspectopn  34026  zarclsun  34029  zarcls  34033  gsumesum  34218  esumlub  34219  esumcst  34222  esumpcvgval  34237  esumgect  34249  esum2d  34252  sigapildsys  34321  sxbrsigalem2  34445  omssubaddlem  34458  omssubadd  34459  eulerpartgbij  34531  actfunsnf1o  34763  actfunsnrndisj  34764  reprsuc  34774  breprexplema  34789  bnj1366  34987  msubco  35727  msubvrs  35756  fin2so  37810  poimirlem17  37840  poimirlem20  37843  cntotbnd  37999  islsat  39319