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

Theorem elrnmpt 5527
 Description: The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015.)
Hypothesis
Ref Expression
rnmpt.1 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
elrnmpt (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem elrnmpt
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2764 . . 3 (𝑦 = 𝐶 → (𝑦 = 𝐵𝐶 = 𝐵))
21rexbidv 3190 . 2 (𝑦 = 𝐶 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
3 rnmpt.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43rnmpt 5526 . 2 ran 𝐹 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
52, 4elab2g 3493 1 (𝐶𝑉 → (𝐶 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝐶 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2139  ∃wrex 3051   ↦ cmpt 4881  ran crn 5267 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-mpt 4882  df-cnv 5274  df-dm 5276  df-rn 5277 This theorem is referenced by:  elrnmpt1s  5528  onnseq  7611  oarec  7813  fifo  8505  infpwfien  9095  fin23lem38  9383  fin1a2lem13  9446  ac6num  9513  isercoll2  14618  iserodd  15762  gsumwspan  17604  odf1o2  18208  mplcoe5lem  19689  neitr  21206  ordtbas2  21217  ordtopn1  21220  ordtopn2  21221  pnfnei  21246  mnfnei  21247  pnrmcld  21368  2ndcomap  21483  dis2ndc  21485  ptpjopn  21637  fbasrn  21909  elfm  21972  rnelfmlem  21977  rnelfm  21978  fmfnfmlem3  21981  fmfnfmlem4  21982  fmfnfm  21983  ptcmplem2  22078  tsmsfbas  22152  ustuqtoplem  22264  utopsnneiplem  22272  utopsnnei  22274  utopreg  22277  fmucnd  22317  neipcfilu  22321  imasdsf1olem  22399  xpsdsval  22407  met1stc  22547  metustel  22576  metustsym  22581  metuel2  22591  metustbl  22592  restmetu  22596  xrtgioo  22830  minveclem3b  23419  uniioombllem3  23573  dvivth  23992  gausslemma2dlem1a  25310  elimampt  29768  acunirnmpt  29789  acunirnmpt2  29790  acunirnmpt2f  29791  locfinreflem  30237  ordtconnlem1  30300  esumcst  30455  esumrnmpt2  30460  measdivcstOLD  30617  oms0  30689  omssubadd  30692  cvmsss2  31584  poimirlem16  33756  poimirlem19  33759  poimirlem24  33764  poimirlem27  33767  itg2addnclem2  33793  nelrnmpt  39774  suprnmpt  39872  rnmptpr  39875  elrnmptd  39883  rnmptssrn  39885  wessf1ornlem  39888  disjrnmpt2  39892  disjf1o  39895  disjinfi  39897  choicefi  39909  rnmptlb  39970  rnmptbddlem  39972  rnmptbd2lem  39980  infnsuprnmpt  39982  elmptima  39990  supxrleubrnmpt  40148  suprleubrnmpt  40165  infrnmptle  40166  infxrunb3rnmpt  40171  supminfrnmpt  40188  infxrgelbrnmpt  40199  infrpgernmpt  40211  supminfxrrnmpt  40217  stoweidlem27  40765  stoweidlem31  40769  stoweidlem35  40773  stirlinglem5  40816  stirlinglem13  40824  fourierdlem53  40897  fourierdlem80  40924  fourierdlem93  40937  fourierdlem103  40947  fourierdlem104  40948  subsaliuncllem  41096  subsaliuncl  41097  sge0rnn0  41106  sge00  41114  fsumlesge0  41115  sge0tsms  41118  sge0cl  41119  sge0f1o  41120  sge0fsum  41125  sge0supre  41127  sge0rnbnd  41131  sge0pnffigt  41134  sge0lefi  41136  sge0ltfirp  41138  sge0resplit  41144  sge0split  41147  sge0reuz  41185  sge0reuzb  41186  hoidmvlelem2  41334  smfpimcc  41538
 Copyright terms: Public domain W3C validator