MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrnmpti Structured version   Visualization version   GIF version

Theorem elrnmpti 5819
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
StepHypRef Expression
1 elrnmpti.2 . . 3 𝐵 ∈ V
21rgenw 3145 . 2 𝑥𝐴 𝐵 ∈ V
3 rnmpt.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43elrnmptg 5818 . 2 (∀𝑥𝐴 𝐵 ∈ V → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
52, 4ax-mp 5 1 (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wcel 2115  wral 3133  wrex 3134  Vcvv 3480  cmpt 5132  ran crn 5543
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-v 3482  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-br 5053  df-opab 5115  df-mpt 5133  df-cnv 5550  df-dm 5552  df-rn 5553
This theorem is referenced by:  fliftel  7055  oarec  8184  unfilem1  8779  pwfilem  8815  elrest  16701  psgneldm2  18632  psgnfitr  18645  iscyggen2  19000  iscyg3  19005  cycsubgcyg  19021  eldprd  19126  leordtval2  21823  iocpnfordt  21826  icomnfordt  21827  lecldbas  21830  tsmsxplem1  22764  minveclem2  24036  lhop2  24624  taylthlem2  24975  fsumvma  25803  dchrptlem2  25855  2sqlem1  26007  dchrisum0fno1  26101  minvecolem2  28664  swrdrn3  30643  rspectopn  31045  gsumesum  31378  esumlub  31379  esumcst  31382  esumpcvgval  31397  esumgect  31409  esum2d  31412  sigapildsys  31481  sxbrsigalem2  31604  omssubaddlem  31617  omssubadd  31618  eulerpartgbij  31690  actfunsnf1o  31935  actfunsnrndisj  31936  reprsuc  31946  breprexplema  31961  bnj1366  32161  msubco  32838  msubvrs  32867  fin2so  34992  poimirlem17  35022  poimirlem20  35025  cntotbnd  35182  islsat  36235
  Copyright terms: Public domain W3C validator