Theorem elrnmpti 5832

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

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  Vcvv 3494   ↦ cmpt 5146  ran crn 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-mpt 5147  df-cnv 5563  df-dm 5565  df-rn 5566

This theorem is referenced by:  fliftel  7062  oarec  8188  unfilem1  8782  pwfilem  8818  elrest  16701  psgneldm2  18632  psgnfitr  18645  iscyggen2  19000  iscyg3  19005  cycsubgcyg  19021  eldprd  19126  leordtval2  21820  iocpnfordt  21823  icomnfordt  21824  lecldbas  21827  tsmsxplem1  22761  minveclem2  24029  lhop2  24612  taylthlem2  24962  fsumvma  25789  dchrptlem2  25841  2sqlem1  25993  dchrisum0fno1  26087  minvecolem2  28652  swrdrn3  30629  gsumesum  31318  esumlub  31319  esumcst  31322  esumpcvgval  31337  esumgect  31349  esum2d  31352  sigapildsys  31421  sxbrsigalem2  31544  omssubaddlem  31557  omssubadd  31558  eulerpartgbij  31630  actfunsnf1o  31875  actfunsnrndisj  31876  reprsuc  31886  breprexplema  31901  bnj1366  32101  msubco  32778  msubvrs  32807  fin2so  34894  poimirlem17  34924  poimirlem20  34927  cntotbnd  35089  islsat  36142